Theorem rabeq 3102

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 2624	. 2 |- F/_ x A
2		nfcv 2624	. 2 |- F/_ x B
3	1, 2	rabeqf 3101	1 |- ( A = B -> { x e. A | ph } = { x e. B | ph } )

Syntax hints:   -> wi 4   = wceq 1374   {crab 2813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rab 2818

This theorem is referenced by:  rabeqbidv  3103  rabeqbidva  3104  difeq1  3610  ifeq1  3938  ifeq2  3939  rabsnif  4091  elfvmptrab  5964  supp0  6898  suppvalfn  6900  suppsnop  6907  fnsuppres  6919  pmvalg  7423  supeq2  7899  oieq2  7929  cantnffval  8071  scott0  8295  hsmex2  8804  iooval2  11553  fzval2  11666  hashbc  12457  elovmpt2wrd  12537  dfphi2  14154  phimullem  14159  mrcfval  14854  mrisval  14876  ipoval  15632  pmtrfval  16266  psgnfval  16316  pmtrsn  16335  lspfval  17397  lsppropd  17442  rrgval  17701  aspval  17743  psrval  17777  mvrfval  17842  ltbval  17902  opsrval  17905  dsmmbas2  18530  dsmmelbas  18532  frlmbas  18548  frlmbasOLD  18549  m1detdiag  18861  clsfval  19287  ordtrest  19464  ordtrest2lem  19465  ordtrest2  19466  xkoval  19818  xkopt  19886  qtopres  19929  kqval  19957  tsmsval2  20358  cncfval  21122  isphtpy  21211  cfilfval  21433  iscmet  21453  ttgval  23849  eengv  23953  isumgra  23980  isuslgra  24008  isusgra  24009  edgss  24017  wwlkn  24346  clwwlkn  24431  clwwlknprop  24436  hashecclwwlkn1  24498  usghashecclwwlk  24499  rusgrasn  24609  numclwwlkovf2  24749  numclwwlkqhash  24765  ordtprsval  27524  ordtrestNEW  27527  ordtrest2NEWlem  27528  omsval  27892  orrvcval4  28031  orrvcoel  28032  orrvccel  28033  snmlfval  28403  funray  29355  fvray  29356  itg2addnclem2  29633  isptfin  29756  islocfin  29757  cntotbnd  29884  pellfundval  30409  elmnc  30681  rgspnval  30713  isfusgra  31828  usgfis  31842  rmsuppss  31913  mndpsuppss  31914  scmsuppss  31915  dmatALTval  31951  dmatALTbas  31952  docaffvalN  35795  docafvalN  35796  lcfr  36259  hlhilocv  36634