Theorem r19.21v 3162

Description: Restricted quantifier version of 19.21v 1941. (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 3151	. . 3 ⊢ (𝜑 → (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → ∀𝑥 ∈ 𝐴 𝜓))
3	2	com12 32	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) → (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))
4		pm2.21 123	. . . 4 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))
5	4	ralrimivw 3133	. . 3 ⊢ (¬ 𝜑 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
6		ax-1 6	. . . 4 ⊢ (𝜓 → (𝜑 → 𝜓))
7	6	ralimi 3074	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
8	5, 7	ja 186	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) → ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓))
9	3, 8	impbii 209	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3052

This theorem is referenced by:  r19.23v  3164  r19.32v  3170  cbvraldva  3217  rmo4  3676  2reu5lem3  3703  ra4v  3823  rmo3  3827  dftr5  5196  reusv3  5347  tfinds2  7815  tfinds3  7816  fpr3g  8235  wfr3g  8269  tfrlem1  8315  tfr3  8338  oeordi  8523  naddssim  8621  ordiso2  9430  ordtypelem7  9439  cantnf  9614  dfac12lem3  10068  ttukeylem5  10435  ttukeylem6  10436  fpwwe2lem7  10560  grudomon  10740  raluz2  12847  bpolycl  16017  ndvdssub  16378  gcdcllem1  16468  acsfn2  17629  pgpfac1  20057  pgpfac  20061  isdomn5  20687  isdomn2OLD  20689  islindf4  21818  isclo2  23053  1stccn  23428  kgencn  23521  txflf  23971  fclsopn  23979  conway  27771  nn0min  32894  bnj580  35055  bnj852  35063  rdgprc  35974  filnetlem4  36563  poimirlem29  37970  heicant  37976  indstrd  42632  ntrneixb  44522  trfr  45389  modelac8prim  45419  2rexrsb  47550  tfis2d  50155