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  17604  pgpfac1  19996  pgpfac  20000  isdomn5  20630  isdomn2OLD  20632  islindf4  21780  isclo2  23008  1stccn  23383  kgencn  23476  txflf  23926  fclsopn  23934  conway  27745  nn0min  32795  bnj580  34896  bnj852  34904  rdgprc  35775  filnetlem4  36362  poimirlem29  37636  heicant  37642  indstrd  42174  ntrneixb  44077  trfr  44945  modelac8prim  44975  2rexrsb  47096  tfis2d  49662