Theorem r19.21v 3189

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939

This proof depends on definitions:  df-bi 210  df-an 401  df-ral 3079

This theorem is used by:  r19.23v  3191  r19.32v  3197  cbvraldva  3244  rmo4  3692  2reu5lem3  3719  ra4v  3837  rmo3  3841  dftr5  5221  reusv3  5375  tfinds2  7858  tfinds3  7859  fpr3g  8280  wfr3g  8314  tfrlem1  8360  tfr3  8384  oeordi  8571  naddssim  8670  ordiso2  9475  ordtypelem7  9484  cantnf  9660  dfac12lem3  10136  ttukeylem5  10503  ttukeylem6  10504  fpwwe2lem7  10628  grudomon  10808  raluz2  12927  bpolycl  16112  ndvdssub  16473  gcdcllem1  16563  acsfn2  17725  pgpfac1  20158  pgpfac  20162  isdomn5  20820  islindf4  21999  isclo2  23256  1stccn  23631  kgencn  23724  txflf  24174  fclsopn  24182  conway  27983  nn0min  33176  bnj580  35310  bnj852  35318  rdgprc  36292  filnetlem4  36920  poimirlem29  38328  heicant  38334  indstrd  42988  ntrneixb  44849  trfr  45699  modelac8prim  45729  2rexrsb  47867  tfis2d  50486