Theorem raleq 2665

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

Assertion

Ref	Expression
raleq	|- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) )

Distinct variable groups:   x, A   x, B

Allowed substitution hint:   ph( x)

Proof of Theorem raleq

Step	Hyp	Ref	Expression
1		nfcv 2312	. 2 |- F/_ x A
2		nfcv 2312	. 2 |- F/_ x B
3	1, 2	raleqf 2661	1 |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1348   A.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  3832  iineq1  3885  bnd2  4157  frforeq2  4328  weeq2  4340  ordeq  4355  reg2exmid  4518  reg3exmid  4562  omsinds  4604  fncnv  5262  funimaexglem  5279  isoeq4  5781  acexmidlemv  5849  tfrlem1  6285  tfr0dm  6299  tfrlemisucaccv  6302  tfrlemi1  6309  tfrlemi14d  6310  tfrexlem  6311  tfr1onlemsucaccv  6318  tfr1onlemaccex  6325  tfr1onlemres  6326  tfrcllemsucaccv  6331  tfrcllembxssdm  6333  tfrcllemaccex  6338  tfrcllemres  6339  tfrcldm  6340  ixpeq1  6684  ac6sfi  6873  fimax2gtri  6876  dcfi  6955  supeq1  6960  supeq2  6963  nnnninfeq2  7102  isomni  7109  ismkv  7126  iswomni  7138  sup3exmid  8862  rexanuz  10941  rexfiuz  10942  fimaxre2  11179  modfsummod  11410  mhmpropd  12678  cnprcl2k  12961  ispsmet  13078  ismet  13099  isxmet  13100  cncfval  13314  dvcn  13419  setindis  13964  bdsetindis  13966  strcoll2  13980  strcollnfALT  13983