Theorem r19.21v 3187

Description: Restricted quantifier version of 19.21v 1972. (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 3176	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 33	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 124	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3158	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3099	. . 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 3076

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 1943

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

This theorem is used by:  r19.23v  3189  r19.32v  3195  cbvraldva  3242  rmo4  3688  2reu5lem3  3715  ra4v  3832  rmo3  3836  dftr5  5216  reusv3  5370  tfinds2  7860  tfinds3  7861  fpr3g  8284  wfr3g  8318  tfrlem1  8364  tfr3  8388  oeordi  8575  naddssim  8674  ordiso2  9487  ordtypelem7  9496  cantnf  9672  dfac12lem3  10148  ttukeylem5  10515  ttukeylem6  10516  fpwwe2lem7  10646  grudomon  10826  raluz2  12946  bpolycl  16138  ndvdssub  16499  gcdcllem1  16589  acsfn2  17751  pgpfac1  20209  pgpfac  20213  isdomn5  20872  islindf4  22051  isclo2  23313  1stccn  23689  kgencn  23782  txflf  24232  fclsopn  24240  conway  28044  nn0min  33291  bnj580  35422  bnj852  35430  rdgprc  36371  filnetlem4  37000  poimirlem29  38398  heicant  38404  indstrd  43059  ntrneixb  44935  trfr  45785  modelac8prim  45815  2rexrsb  47990  tfis2d  50606