Theorem r19.21v 3159

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 3148	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 32	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 123	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3130	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3067	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
8	5, 7	ja 186	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
9	3, 8	impbii 209	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

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

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 3046

This theorem is referenced by:  r19.23v  3162  r19.32v  3171  cbvraldva  3218  rmo4  3704  2reu5lem3  3731  ra4v  3851  rmo3  3855  dftr5  5221  dftr5OLD  5222  reusv3  5363  tfinds2  7843  tfinds3  7844  fpr3g  8267  wfr3g  8301  tfrlem1  8347  tfr3  8370  oeordi  8554  naddssim  8652  ordiso2  9475  ordtypelem7  9484  cantnf  9653  dfac12lem3  10106  ttukeylem5  10473  ttukeylem6  10474  fpwwe2lem7  10597  grudomon  10777  raluz2  12863  bpolycl  16025  ndvdssub  16386  gcdcllem1  16476  acsfn2  17631  pgpfac1  20019  pgpfac  20023  isdomn5  20626  isdomn2OLD  20628  islindf4  21754  isclo2  22982  1stccn  23357  kgencn  23450  txflf  23900  fclsopn  23908  conway  27718  nn0min  32752  bnj580  34910  bnj852  34918  rdgprc  35789  filnetlem4  36376  poimirlem29  37650  heicant  37656  indstrd  42188  ntrneixb  44091  trfr  44959  modelac8prim  44989  2rexrsb  47107  tfis2d  49673