Theorem raleq 2728

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 2372	. 2 |- F/_ x A
2		nfcv 2372	. 2 |- F/_ x B
3	1, 2	raleqf 2724	1 |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1395   A.wral 2508

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513

This theorem is referenced by:  raleqi  2732  raleqdv  2734  raleqbi1dv  2740  sbralie  2783  inteq  3926  iineq1  3979  bnd2  4257  frforeq2  4436  weeq2  4448  ordeq  4463  reg2exmid  4628  reg3exmid  4672  omsinds  4714  fncnv  5387  funimaexglem  5404  isoeq4  5928  acexmidlemv  5999  tfrlem1  6454  tfr0dm  6468  tfrlemisucaccv  6471  tfrlemi1  6478  tfrlemi14d  6479  tfrexlem  6480  tfr1onlemsucaccv  6487  tfr1onlemaccex  6494  tfr1onlemres  6495  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllemaccex  6507  tfrcllemres  6508  tfrcldm  6509  ixpeq1  6856  ac6sfi  7060  fimax2gtri  7063  dcfi  7148  supeq1  7153  supeq2  7156  nnnninfeq2  7296  isomni  7303  ismkv  7320  iswomni  7332  acneq  7384  tapeq2  7439  sup3exmid  9104  rexanuz  11499  rexfiuz  11500  fimaxre2  11738  modfsummod  11969  mhmpropd  13499  isghm  13780  iscmn  13830  srgideu  13935  dfrhm2  14118  cnprcl2k  14880  ispsmet  14997  ismet  15018  isxmet  15019  cncfval  15246  dvcn  15374  setindis  16330  bdsetindis  16332  strcoll2  16346  strcollnfALT  16349