Theorem r19.21v 3102

Description: Restricted quantifier version of 19.21v 1945. (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 388	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓)))
2	1	albii 1825	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ ∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓)))
3		19.21v 1945	. . 3 ⊢ (∀𝑥(𝜑 → (𝑥 ∈ 𝐴 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)))
4	2, 3	bitri 274	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)))
5		df-ral 3070	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 → 𝜓)))
6		df-ral 3070	. . 3 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
7	6	imbi2i 335	. 2 ⊢ ((𝜑 → ∀𝑥 ∈ 𝐴 𝜓) ↔ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓)))
8	4, 5, 7	3bitr4i 302	1 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   ∈ wcel 2109  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916

This theorem depends on definitions:  df-bi 206  df-ex 1786  df-ral 3070

This theorem is referenced by:  r19.23v  3209  r19.32v  3269  rmo4  3668  2reu5lem3  3695  ra4v  3822  rmo3  3826  dftr5  5198  reusv3  5331  tfinds2  7698  tfinds3  7699  fpr3g  8085  wfr3g  8122  tfrlem1  8191  tfr3  8214  oeordi  8394  ordiso2  9235  ordtypelem7  9244  cantnf  9412  dfac12lem3  9885  ttukeylem5  10253  ttukeylem6  10254  fpwwe2lem7  10377  grudomon  10557  raluz2  12619  bpolycl  15743  ndvdssub  16099  gcdcllem1  16187  acsfn2  17353  pgpfac1  19664  pgpfac  19668  isdomn2  20551  islindf4  21026  isclo2  22220  1stccn  22595  kgencn  22688  txflf  23138  fclsopn  23146  nn0min  31113  bnj580  32872  bnj852  32880  rdgprc  33749  naddssim  33816  conway  33972  filnetlem4  34549  poimirlem29  35785  heicant  35791  isdomn5  40151  ntrneixb  41658  2rexrsb  44545  tfis2d  46338