Theorem raleq 2665

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 2312	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2312	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	raleqf 2661	1 ⊢ (𝐴 = 𝐵 → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1348  ∀wral 2448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453

This theorem is referenced by:  raleqi  2669  raleqdv  2671  raleqbi1dv  2673  sbralie  2714  inteq  3834  iineq1  3887  bnd2  4159  frforeq2  4330  weeq2  4342  ordeq  4357  reg2exmid  4520  reg3exmid  4564  omsinds  4606  fncnv  5264  funimaexglem  5281  isoeq4  5783  acexmidlemv  5851  tfrlem1  6287  tfr0dm  6301  tfrlemisucaccv  6304  tfrlemi1  6311  tfrlemi14d  6312  tfrexlem  6313  tfr1onlemsucaccv  6320  tfr1onlemaccex  6327  tfr1onlemres  6328  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllemaccex  6340  tfrcllemres  6341  tfrcldm  6342  ixpeq1  6687  ac6sfi  6876  fimax2gtri  6879  dcfi  6958  supeq1  6963  supeq2  6966  nnnninfeq2  7105  isomni  7112  ismkv  7129  iswomni  7141  sup3exmid  8873  rexanuz  10952  rexfiuz  10953  fimaxre2  11190  modfsummod  11421  mhmpropd  12689  cnprcl2k  13000  ispsmet  13117  ismet  13138  isxmet  13139  cncfval  13353  dvcn  13458  setindis  14002  bdsetindis  14004  strcoll2  14018  strcollnfALT  14021