Theorem r19.21v 3164

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207  ∀wral 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ral 3054

This theorem is referenced by:  r19.23v  3166  r19.32v  3172  cbvraldva  3219  rmo4  3671  2reu5lem3  3698  ra4v  3817  rmo3  3821  dftr5  5183  reusv3  5334  tfinds2  7804  tfinds3  7805  fpr3g  8225  wfr3g  8259  tfrlem1  8305  tfr3  8328  oeordi  8513  naddssim  8611  ordiso2  9420  ordtypelem7  9429  cantnf  9605  dfac12lem3  10059  ttukeylem5  10426  ttukeylem6  10427  fpwwe2lem7  10551  grudomon  10731  raluz2  12838  bpolycl  16008  ndvdssub  16369  gcdcllem1  16459  acsfn2  17620  pgpfac1  20048  pgpfac  20052  isdomn5  20682  isdomn2OLD  20684  islindf4  21813  isclo2  23071  1stccn  23446  kgencn  23539  txflf  23989  fclsopn  23997  conway  27789  nn0min  32913  bnj580  35095  bnj852  35103  rdgprc  36020  filnetlem4  36609  poimirlem29  38016  heicant  38022  indstrd  42678  ntrneixb  44539  trfr  45406  modelac8prim  45436  2rexrsb  47565  tfis2d  50170