Theorem r19.21v 3187

Description: Restricted quantifier version of 19.21v 1959. (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 42	. . . 4 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
2	1	ralimdv 3176	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 32	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 123	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3158	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3099	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
8	5, 7	ja 187	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
9	3, 8	impbii 211	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208  ∀wral 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3077

This theorem is referenced by:  r19.23v  3189  r19.32v  3195  cbvraldva  3242  rmo4  3693  2reu5lem3  3720  ra4v  3838  rmo3  3842  dftr5  5211  reusv3  5362  tfinds2  7844  tfinds3  7845  fpr3g  8266  wfr3g  8300  tfrlem1  8346  tfr3  8370  oeordi  8557  naddssim  8656  ordiso2  9463  ordtypelem7  9472  cantnf  9648  dfac12lem3  10102  ttukeylem5  10470  ttukeylem6  10471  fpwwe2lem7  10595  grudomon  10775  raluz2  12898  bpolycl  16082  ndvdssub  16443  gcdcllem1  16533  acsfn2  17695  pgpfac1  20122  pgpfac  20126  isdomn5  20756  isdomn2OLD  20758  islindf4  21887  isclo2  23145  1stccn  23520  kgencn  23613  txflf  24063  fclsopn  24071  conway  27869  nn0min  33020  bnj580  35205  bnj852  35213  rdgprc  36139  filnetlem4  36738  poimirlem29  38145  heicant  38151  indstrd  42807  ntrneixb  44668  trfr  45535  modelac8prim  45565  2rexrsb  47693  tfis2d  50298