Theorem r19.21v 3187

Description: Restricted quantifier version of 19.21v 1971. (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 3176	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 33	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 124	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3158	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3099	. . 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 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  r19.23v  3189  r19.32v  3195  cbvraldva  3242  rmo4  3687  2reu5lem3  3714  ra4v  3832  rmo3  3836  dftr5  5215  reusv3  5367  tfinds2  7879  tfinds3  7880  fpr3g  8310  wfr3g  8344  tfrlem1  8390  tfr3  8414  oeordi  8603  naddssim  8702  ordiso2  9516  ordtypelem7  9525  cantnf  9701  dfac12lem3  10231  ttukeylem5  10598  ttukeylem6  10599  fpwwe2lem7  10729  grudomon  10909  raluz2  13031  bpolycl  16227  ndvdssub  16588  gcdcllem1  16678  acsfn2  17846  pgpfac1  20305  pgpfac  20309  isdomn5  20971  islindf4  22153  isclo2  23415  1stccn  23791  kgencn  23884  txflf  24334  fclsopn  24342  conway  28174  nn0min  33462  bnj580  35593  bnj852  35601  rdgprc  36652  filnetlem4  37265  poimirlem29  38676  heicant  38682  indstrd  43352  ntrneixb  45204  trfr  46060  modelac8prim  46090  2rexrsb  48281  tfis2d  50970