Theorem rabeq 3038

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

Syntax hints:   -> wi 4   = wceq 1444   {crab 2741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-rab 2746

This theorem is referenced by:  rabeqdv  3039  rabeqbidv  3040  rabeqbidva  3041  difeq1  3544  ifeq1  3885  ifeq2  3886  rabsnif  4041  elfvmptrab  5971  supp0  6919  suppvalfn  6921  suppsnop  6928  fnsuppres  6942  pmvalg  7483  supeq2  7962  oieq2  8028  cantnffval  8168  scott0  8357  hsmex2  8863  iooval2  11669  fzval2  11787  hashbc  12616  elovmpt2wrd  12709  phimullem  14727  mrcfval  15514  ipoval  16400  pmtrfval  17091  psgnfval  17141  pmtrsn  17160  lspfval  18196  lsppropd  18241  rrgval  18511  aspval  18552  psrval  18586  mvrfval  18644  ltbval  18695  opsrval  18698  dsmmbas2  19300  dsmmelbas  19302  frlmbas  19318  m1detdiag  19622  clsfval  20040  ordtrest  20218  ordtrest2lem  20219  ordtrest2  20220  isptfin  20531  islocfin  20532  xkoval  20602  xkopt  20670  qtopres  20713  kqval  20741  tsmsval2  21144  cncfval  21920  isphtpy  22012  cfilfval  22234  iscmet  22254  ttgval  24905  isumgra  25042  isuslgra  25070  isusgra  25071  edgss  25079  wwlkn  25410  clwwlkn  25495  clwwlknprop  25500  hashecclwwlkn1  25562  usghashecclwwlk  25563  rusgrasn  25673  numclwwlkovf2  25812  numclwwlkqhash  25828  ordtprsval  28724  ordtrestNEW  28727  ordtrest2NEWlem  28728  omsval  29117  omsvalOLD  29121  orrvcval4  29297  orrvcoel  29298  orrvccel  29299  snmlfval  30053  funray  30907  fvray  30908  itg2addnclem2  31994  cntotbnd  32128  docaffvalN  34689  docafvalN  34690  lcfr  35153  hlhilocv  35528  pellfundval  35727  pellfundvalOLD  35728  elmnc  35995  rgspnval  36034  rabeqd  37377  dvnprodlem1  37821  dvnprodlem2  37822  dvnprodlem3  37823  dvnprod  37824  uvtxa0  39466  cusgredg  39492  isfusgra  39789  usgfis  39811  usgfisALT  39815  assintopmap  39895  rmsuppss  40208  mndpsuppss  40209  scmsuppss  40210  dmatALTval  40246  dmatALTbas  40247