Theorem r19.21v 3086

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

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1618   ∈ wcel 2127  ∀wral 3038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976

This theorem depends on definitions:  df-bi 197  df-ex 1842  df-ral 3043

This theorem is referenced by:  r19.23v  3149  r19.32v  3209  rmo4  3528  2reu5lem3  3544  ra4v  3653  rmo3  3657  dftr5  4895  reusv3  5013  tfinds2  7216  tfinds3  7217  wfr3g  7570  tfrlem1  7629  tfr3  7652  oeordi  7824  ordiso2  8573  ordtypelem7  8582  cantnf  8751  dfac12lem3  9130  ttukeylem5  9498  ttukeylem6  9499  fpwwe2lem8  9622  grudomon  9802  raluz2  11901  bpolycl  14953  ndvdssub  15306  gcdcllem1  15394  acsfn2  16496  pgpfac1  18650  pgpfac  18654  isdomn2  19472  islindf4  20350  isclo2  21065  1stccn  21439  kgencn  21532  txflf  21982  fclsopn  21990  nn0min  29847  bnj580  31261  bnj852  31269  rdgprc  31976  conway  32187  filnetlem4  32653  poimirlem29  33720  heicant  33726  ntrneixb  38864  2rexrsb  41646  tfis2d  42906