Theorem r19.21v 3191

Description: Restricted quantifier version of 19.21v 1974. (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 43	. . . 4 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
2	1	ralimdv 3180	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 33	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 124	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3162	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3103	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
8	5, 7	ja 188	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
9	3, 8	impbii 212	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wral 3080

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3081

This theorem is used by:  r19.23v  3193  r19.32v  3199  cbvraldva  3246  rmo4  3691  2reu5lem3  3718  ra4v  3836  rmo3  3840  dftr5  5222  reusv3  5374  tfinds2  7909  tfinds3  7910  fpr3g  8341  wfr3g  8375  tfrlem1  8421  tfr3  8445  oeordi  8634  naddssim  8733  ordiso2  9546  ordtypelem7  9555  cantnf  9731  dfac12lem3  10263  ttukeylem5  10630  ttukeylem6  10631  fpwwe2lem7  10761  grudomon  10941  raluz2  13064  bpolycl  16262  ndvdssub  16623  gcdcllem1  16713  acsfn2  17887  pgpfac1  20347  pgpfac  20351  isdomn5  21013  islindf4  22199  isclo2  23461  1stccn  23837  kgencn  23930  txflf  24380  fclsopn  24388  conway  28222  nn0min  33508  bnj580  35654  bnj852  35662  rdgprc  36771  filnetlem4  37384  poimirlem29  38835  heicant  38841  indstrd  43509  ntrneixb  45356  trfr  46216  modelac8prim  46246  2rexrsb  48446  tfis2d  51193