Theorem r19.21v 3192

Description: Restricted quantifier version of 19.21v 1972. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 2-Jan-2020.) (Proof shortened by Wolf Lammen, 11-Dec-2024.)

Assertion

Ref	Expression
r19.21v	⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.21v

Step	Hyp	Ref	Expression
1		pm2.27 43	. . . 4 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
2	1	ralimdv 3181	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 33	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 124	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3163	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3104	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
8	5, 7	ja 188	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
9	3, 8	impbii 212	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wral 3081

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3082

This theorem is used by:  r19.23v  3194  r19.32v  3200  cbvraldva  3247  rmo4  3695  2reu5lem3  3722  ra4v  3839  rmo3  3843  dftr5  5224  reusv3  5378  tfinds2  7866  tfinds3  7867  fpr3g  8288  wfr3g  8322  tfrlem1  8368  tfr3  8392  oeordi  8579  naddssim  8678  ordiso2  9484  ordtypelem7  9493  cantnf  9669  dfac12lem3  10145  ttukeylem5  10512  ttukeylem6  10513  fpwwe2lem7  10637  grudomon  10817  raluz2  12937  bpolycl  16128  ndvdssub  16489  gcdcllem1  16579  acsfn2  17741  pgpfac1  20196  pgpfac  20200  isdomn5  20859  islindf4  22038  isclo2  23295  1stccn  23671  kgencn  23764  txflf  24214  fclsopn  24222  conway  28023  nn0min  33235  bnj580  35366  bnj852  35374  rdgprc  36321  filnetlem4  36949  poimirlem29  38357  heicant  38363  indstrd  43018  ntrneixb  44879  trfr  45729  modelac8prim  45759  2rexrsb  47897  tfis2d  50515