Theorem r19.21v 3154

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206  ∀wral 3044

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045

This theorem is referenced by:  r19.23v  3156  r19.32v  3162  cbvraldva  3209  rmo4  3690  2reu5lem3  3717  ra4v  3837  rmo3  3841  dftr5  5203  reusv3  5344  tfinds2  7797  tfinds3  7798  fpr3g  8218  wfr3g  8252  tfrlem1  8298  tfr3  8321  oeordi  8505  naddssim  8603  ordiso2  9407  ordtypelem7  9416  cantnf  9589  dfac12lem3  10040  ttukeylem5  10407  ttukeylem6  10408  fpwwe2lem7  10531  grudomon  10711  raluz2  12798  bpolycl  15959  ndvdssub  16320  gcdcllem1  16410  acsfn2  17569  pgpfac1  19961  pgpfac  19965  isdomn5  20595  isdomn2OLD  20597  islindf4  21745  isclo2  22973  1stccn  23348  kgencn  23441  txflf  23891  fclsopn  23899  conway  27710  nn0min  32765  bnj580  34880  bnj852  34888  rdgprc  35768  filnetlem4  36355  poimirlem29  37629  heicant  37635  indstrd  42166  ntrneixb  44068  trfr  44936  modelac8prim  44966  2rexrsb  47086  tfis2d  49665