Theorem r19.21v 3158

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 3147	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 32	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 123	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3129	. . 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  3160  r19.32v  3168  cbvraldva  3215  rmo4  3698  2reu5lem3  3725  ra4v  3845  rmo3  3849  dftr5  5213  dftr5OLD  5214  reusv3  5355  tfinds2  7820  tfinds3  7821  fpr3g  8241  wfr3g  8275  tfrlem1  8321  tfr3  8344  oeordi  8528  naddssim  8626  ordiso2  9444  ordtypelem7  9453  cantnf  9622  dfac12lem3  10075  ttukeylem5  10442  ttukeylem6  10443  fpwwe2lem7  10566  grudomon  10746  raluz2  12832  bpolycl  15994  ndvdssub  16355  gcdcllem1  16445  acsfn2  17600  pgpfac1  19988  pgpfac  19992  isdomn5  20595  isdomn2OLD  20597  islindf4  21723  isclo2  22951  1stccn  23326  kgencn  23419  txflf  23869  fclsopn  23877  conway  27687  nn0min  32718  bnj580  34876  bnj852  34884  rdgprc  35755  filnetlem4  36342  poimirlem29  37616  heicant  37622  indstrd  42154  ntrneixb  44057  trfr  44925  modelac8prim  44955  2rexrsb  47076  tfis2d  49642