Theorem r19.21v 3190

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209  ∀wral 3079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3080

This theorem is referenced by:  r19.23v  3192  r19.32v  3198  cbvraldva  3245  rmo4  3693  2reu5lem3  3720  ra4v  3838  rmo3  3842  dftr5  5222  reusv3  5376  tfinds2  7856  tfinds3  7857  fpr3g  8278  wfr3g  8312  tfrlem1  8358  tfr3  8382  oeordi  8569  naddssim  8668  ordiso2  9473  ordtypelem7  9482  cantnf  9658  dfac12lem3  10125  ttukeylem5  10492  ttukeylem6  10493  fpwwe2lem7  10617  grudomon  10797  raluz2  12916  bpolycl  16101  ndvdssub  16462  gcdcllem1  16552  acsfn2  17714  pgpfac1  20147  pgpfac  20151  isdomn5  20809  islindf4  21988  isclo2  23245  1stccn  23620  kgencn  23713  txflf  24163  fclsopn  24171  conway  27972  nn0min  33165  bnj580  35301  bnj852  35309  rdgprc  36284  filnetlem4  36892  poimirlem29  38300  heicant  38306  indstrd  42960  ntrneixb  44821  trfr  45671  modelac8prim  45701  2rexrsb  47839  tfis2d  50458