Theorem r19.21v 3175

Description: Restricted quantifier version of 19.21v 1940. (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.)

Assertion

Ref	Expression
r19.21v	⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem r19.21v

Step	Hyp	Ref	Expression
1		bi2.04 391	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)))
2	1	albii 1820	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ ∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓)))
3		19.21v 1940	. . 3 ⊢ (∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)))
4	2, 3	bitri 277	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)))
5		df-ral 3143	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)))
6		df-ral 3143	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
7	6	imbi2i 338	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)))
8	4, 5, 7	3bitr4i 305	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535   ∈ wcel 2114  ∀wral 3138

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-ral 3143

This theorem is referenced by:  r19.23v  3279  r19.32v  3340  rmo4  3721  2reu5lem3  3748  ra4v  3868  rmo3  3872  rmo3OLD  3873  dftr5  5175  reusv3  5306  tfinds2  7578  tfinds3  7579  wfr3g  7953  tfrlem1  8012  tfr3  8035  oeordi  8213  ordiso2  8979  ordtypelem7  8988  cantnf  9156  dfac12lem3  9571  ttukeylem5  9935  ttukeylem6  9936  fpwwe2lem8  10059  grudomon  10239  raluz2  12298  bpolycl  15406  ndvdssub  15760  gcdcllem1  15848  acsfn2  16934  pgpfac1  19202  pgpfac  19206  isdomn2  20072  islindf4  20982  isclo2  21696  1stccn  22071  kgencn  22164  txflf  22614  fclsopn  22622  nn0min  30536  bnj580  32185  bnj852  32193  rdgprc  33039  fpr3g  33122  conway  33264  filnetlem4  33729  poimirlem29  34936  heicant  34942  ntrneixb  40494  2rexrsb  43349  tfis2d  44832