Theorem raleq 2730

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1397   A.wral 2510

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515

This theorem is referenced by:  raleqi  2734  raleqdv  2736  raleqbi1dv  2742  sbralie  2785  inteq  3931  iineq1  3984  bnd2  4263  frforeq2  4442  weeq2  4454  ordeq  4469  reg2exmid  4634  reg3exmid  4678  omsinds  4720  fncnv  5396  funimaexglem  5413  isoeq4  5945  acexmidlemv  6016  tfrlem1  6474  tfr0dm  6488  tfrlemisucaccv  6491  tfrlemi1  6498  tfrlemi14d  6499  tfrexlem  6500  tfr1onlemsucaccv  6507  tfr1onlemaccex  6514  tfr1onlemres  6515  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemaccex  6527  tfrcllemres  6528  tfrcldm  6529  ixpeq1  6878  ac6sfi  7087  fimax2gtri  7091  dcfi  7180  supeq1  7185  supeq2  7188  nnnninfeq2  7328  isomni  7335  ismkv  7352  iswomni  7364  acneq  7417  tapeq2  7472  sup3exmid  9137  rexanuz  11566  rexfiuz  11567  fimaxre2  11805  modfsummod  12037  mhmpropd  13567  isghm  13848  iscmn  13898  srgideu  14004  dfrhm2  14187  cnprcl2k  14949  ispsmet  15066  ismet  15087  isxmet  15088  cncfval  15315  dvcn  15443  setindis  16613  bdsetindis  16615  strcoll2  16629  strcollnfALT  16632