Theorem rabeq 3100

Description: Equality theorem for restricted class abstractions. (Contributed by NM, 15-Oct-2003.)

Assertion

Ref	Expression
rabeq	|- ( A = B -> { x e. A | ph } = { x e. B | ph } )

Distinct variable groups:   x, A   x, B

Allowed substitution hint:   ph( x)

Proof of Theorem rabeq

Step	Hyp	Ref	Expression
1		nfcv 2616	. 2 |- F/_ x A
2		nfcv 2616	. 2 |- F/_ x B
3	1, 2	rabeqf 3099	1 |- ( A = B -> { x e. A | ph } = { x e. B | ph } )

Syntax hints:   -> wi 4   = wceq 1398   {crab 2808

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2813

This theorem is referenced by:  rabeqbidv  3101  rabeqbidva  3102  difeq1  3601  ifeq1  3933  ifeq2  3934  rabsnif  4085  elfvmptrab  5953  supp0  6896  suppvalfn  6898  suppsnop  6905  fnsuppres  6919  pmvalg  7423  supeq2  7899  oieq2  7930  cantnffval  8071  scott0  8295  hsmex2  8804  iooval2  11565  fzval2  11678  hashbc  12486  elovmpt2wrd  12571  dfphi2  14388  phimullem  14393  mrcfval  15097  mrisval  15119  ipoval  15983  pmtrfval  16674  psgnfval  16724  pmtrsn  16743  lspfval  17814  lsppropd  17859  rrgval  18130  aspval  18172  psrval  18206  mvrfval  18271  ltbval  18331  opsrval  18334  dsmmbas2  18941  dsmmelbas  18943  frlmbas  18959  frlmbasOLD  18960  m1detdiag  19266  clsfval  19693  ordtrest  19870  ordtrest2lem  19871  ordtrest2  19872  isptfin  20183  islocfin  20184  xkoval  20254  xkopt  20322  qtopres  20365  kqval  20393  tsmsval2  20794  cncfval  21558  isphtpy  21647  cfilfval  21869  iscmet  21889  ttgval  24380  eengv  24484  isumgra  24517  isuslgra  24545  isusgra  24546  edgss  24554  wwlkn  24884  clwwlkn  24969  clwwlknprop  24974  hashecclwwlkn1  25036  usghashecclwwlk  25037  rusgrasn  25147  numclwwlkovf2  25286  numclwwlkqhash  25302  ordtprsval  28135  ordtrestNEW  28138  ordtrest2NEWlem  28139  omsval  28501  orrvcval4  28667  orrvcoel  28668  orrvccel  28669  snmlfval  29039  funray  30018  fvray  30019  itg2addnclem2  30307  cntotbnd  30532  pellfundval  31055  elmnc  31326  rgspnval  31358  rabeqd  31678  dvnprodlem1  31982  dvnprodlem2  31983  dvnprodlem3  31984  dvnprod  31985  isfusgra  32796  usgfis  32818  usgfisALT  32822  assintopmap  32902  rmsuppss  33217  mndpsuppss  33218  scmsuppss  33219  dmatALTval  33255  dmatALTbas  33256  docaffvalN  37245  docafvalN  37246  lcfr  37709  hlhilocv  38084