Theorem r19.21v 2960

Description: Restricted quantifier version of 19.21v 1868. (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 376	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)))
2	1	albii 1747	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ ∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓)))
3		19.21v 1868	. . 3 ⊢ (∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)))
4	2, 3	bitri 264	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)))
5		df-ral 2917	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)))
6		df-ral 2917	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
7	6	imbi2i 326	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)))
8	4, 5, 7	3bitr4i 292	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1481   ∈ wcel 1990  ∀wral 2912

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

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-ral 2917

This theorem is referenced by:  r19.23v  3023  r19.32v  3083  rmo4  3399  2reu5lem3  3415  ra4v  3524  rmo3  3528  dftr5  4755  reusv3  4876  tfinds2  7063  tfinds3  7064  wfr3g  7413  tfrlem1  7472  tfr3  7495  oeordi  7667  ordiso2  8420  ordtypelem7  8429  cantnf  8590  dfac12lem3  8967  ttukeylem5  9335  ttukeylem6  9336  fpwwe2lem8  9459  grudomon  9639  raluz2  11737  bpolycl  14783  ndvdssub  15133  gcdcllem1  15221  acsfn2  16324  pgpfac1  18479  pgpfac  18483  isdomn2  19299  islindf4  20177  isclo2  20892  1stccn  21266  kgencn  21359  txflf  21810  fclsopn  21818  nn0min  29567  bnj580  30983  bnj852  30991  rdgprc  31700  conway  31910  filnetlem4  32376  poimirlem29  33438  heicant  33444  ntrneixb  38393  2rexrsb  41171  tfis2d  42427