Theorem r19.21v 3157

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  r19.23v  3159  r19.32v  3165  cbvraldva  3212  rmo4  3684  2reu5lem3  3711  ra4v  3831  rmo3  3835  dftr5  5200  reusv3  5341  tfinds2  7794  tfinds3  7795  fpr3g  8215  wfr3g  8249  tfrlem1  8295  tfr3  8318  oeordi  8502  naddssim  8600  ordiso2  9401  ordtypelem7  9410  cantnf  9583  dfac12lem3  10037  ttukeylem5  10404  ttukeylem6  10405  fpwwe2lem7  10528  grudomon  10708  raluz2  12795  bpolycl  15959  ndvdssub  16320  gcdcllem1  16410  acsfn2  17569  pgpfac1  19994  pgpfac  19998  isdomn5  20625  isdomn2OLD  20627  islindf4  21775  isclo2  23003  1stccn  23378  kgencn  23471  txflf  23921  fclsopn  23929  conway  27740  nn0min  32803  bnj580  34925  bnj852  34933  rdgprc  35836  filnetlem4  36423  poimirlem29  37697  heicant  37703  indstrd  42234  ntrneixb  44136  trfr  45003  modelac8prim  45033  2rexrsb  47141  tfis2d  49720