Theorem raleq 2702

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1373   A.wral 2484

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489

This theorem is referenced by:  raleqi  2706  raleqdv  2708  raleqbi1dv  2714  sbralie  2756  inteq  3888  iineq1  3941  bnd2  4218  frforeq2  4393  weeq2  4405  ordeq  4420  reg2exmid  4585  reg3exmid  4629  omsinds  4671  fncnv  5341  funimaexglem  5358  isoeq4  5875  acexmidlemv  5944  tfrlem1  6396  tfr0dm  6410  tfrlemisucaccv  6413  tfrlemi1  6420  tfrlemi14d  6421  tfrexlem  6422  tfr1onlemsucaccv  6429  tfr1onlemaccex  6436  tfr1onlemres  6437  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllemaccex  6449  tfrcllemres  6450  tfrcldm  6451  ixpeq1  6798  ac6sfi  6997  fimax2gtri  7000  dcfi  7085  supeq1  7090  supeq2  7093  nnnninfeq2  7233  isomni  7240  ismkv  7257  iswomni  7269  acneq  7316  tapeq2  7367  sup3exmid  9032  rexanuz  11332  rexfiuz  11333  fimaxre2  11571  modfsummod  11802  mhmpropd  13331  isghm  13612  iscmn  13662  srgideu  13767  dfrhm2  13949  cnprcl2k  14711  ispsmet  14828  ismet  14849  isxmet  14850  cncfval  15077  dvcn  15205  setindis  15940  bdsetindis  15942  strcoll2  15956  strcollnfALT  15959