Theorem r19.21v 3188

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 3177	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 33	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 124	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3159	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3100	. . 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 3077

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 3078

This theorem is used by:  r19.23v  3190  r19.32v  3196  cbvraldva  3243  rmo4  3688  2reu5lem3  3715  ra4v  3832  rmo3  3836  dftr5  5216  reusv3  5367  tfinds2  7873  tfinds3  7874  fpr3g  8296  wfr3g  8330  tfrlem1  8376  tfr3  8400  oeordi  8589  naddssim  8688  ordiso2  9502  ordtypelem7  9511  cantnf  9687  dfac12lem3  10217  ttukeylem5  10584  ttukeylem6  10585  fpwwe2lem7  10715  grudomon  10895  raluz2  13017  bpolycl  16211  ndvdssub  16572  gcdcllem1  16662  acsfn2  17830  pgpfac1  20289  pgpfac  20293  isdomn5  20955  islindf4  22137  isclo2  23399  1stccn  23775  kgencn  23868  txflf  24318  fclsopn  24326  conway  28158  nn0min  33405  bnj580  35536  bnj852  35544  rdgprc  36536  filnetlem4  37149  poimirlem29  38547  heicant  38553  indstrd  43223  ntrneixb  45080  trfr  45930  modelac8prim  45960  2rexrsb  48141  tfis2d  50756