Theorem r19.21v 3126

Description: Restricted quantifier version of 19.21v 1898. (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 380	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)))
2	1	albii 1782	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ ∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓)))
3		19.21v 1898	. . 3 ⊢ (∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)))
4	2, 3	bitri 267	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)))
5		df-ral 3094	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)))
6		df-ral 3094	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
7	6	imbi2i 328	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)))
8	4, 5, 7	3bitr4i 295	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1505   ∈ wcel 2050  ∀wral 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869

This theorem depends on definitions:  df-bi 199  df-ex 1743  df-ral 3094

This theorem is referenced by:  r19.23v  3225  r19.32v  3282  rmo4  3634  2reu5lem3  3658  ra4v  3772  rmo3  3776  rmo3OLD  3777  dftr5  5033  reusv3  5159  tfinds2  7394  tfinds3  7395  wfr3g  7756  tfrlem1  7816  tfr3  7839  oeordi  8014  ordiso2  8774  ordtypelem7  8783  cantnf  8950  dfac12lem3  9365  ttukeylem5  9733  ttukeylem6  9734  fpwwe2lem8  9857  grudomon  10037  raluz2  12111  bpolycl  15266  ndvdssub  15620  gcdcllem1  15708  acsfn2  16792  pgpfac1  18952  pgpfac  18956  isdomn2  19793  islindf4  20684  isclo2  21400  1stccn  21775  kgencn  21868  txflf  22318  fclsopn  22326  nn0min  30283  bnj580  31829  bnj852  31837  rdgprc  32557  fpr3g  32640  conway  32782  filnetlem4  33247  poimirlem29  34359  heicant  34365  ntrneixb  39805  2rexrsb  42704  tfis2d  44148