Theorem raleqbi1dv 2678

Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)

Hypothesis

Ref	Expression
raleqd.1	⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
raleqbi1dv	⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

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

Proof of Theorem raleqbi1dv

Step	Hyp	Ref	Expression
1		raleq 2670	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))
2		raleqd.1	. . 3 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))
3	2	ralbidv 2475	. 2 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))
4	1, 3	bitrd 188	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1353  ∀wral 2453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458

This theorem is referenced by:  frforeq2  4339  weeq2  4351  peano5  4591  isoeq4  5795  exmidomni  7130  pitonn  7822  peano1nnnn  7826  peano2nnnn  7827  peano5nnnn  7866  peano5nni  8895  1nn  8903  peano2nn  8904  dfuzi  9336  mhmpropd  12729  issubm  12735  iscmn  12904  istopg  13077  isbasisg  13122  basis2  13126  eltg2  13133  ispsmet  13403  ismet  13424  isxmet  13425  metrest  13586  cncfval  13639  bj-indeq  14250  bj-nntrans  14272