Theorem raleq 2522

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

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem raleq

Step	Hyp	Ref	Expression
1		nfcv 2194	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2194	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	raleqf 2518	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 102   = wceq 1259  ∀wral 2323

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038

This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328

This theorem is referenced by:  raleqi  2526  raleqdv  2528  raleqbi1dv  2530  sbralie  2563  inteq  3645  iineq1  3698  bnd2  3953  frforeq2  4109  weeq2  4121  ordeq  4136  reg2exmid  4288  reg3exmid  4331  fncnv  4992  funimaexglem  5009  isoeq4  5471  acexmidlemv  5537  tfrlem1  5953  tfr0  5967  tfrlemisucaccv  5969  tfrlemi1  5976  tfrlemi14d  5977  tfrexlem  5978  ac6sfi  6382  supeq1  6391  supeq2  6394  rexanuz  9808  setindis  10451  bdsetindis  10453  strcoll2  10467