Theorem rabeq 3064

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

Syntax hints:   -> wi 4   = wceq 1370   {crab 2799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804

This theorem is referenced by:  rabeqbidv  3065  rabeqbidva  3066  difeq1  3567  ifeq1  3895  ifeq2  3896  rabsnif  4044  supp0  6797  suppvalfn  6799  suppsnop  6806  fnsuppres  6818  pmvalg  7327  supeq2  7801  oieq2  7830  cantnffval  7972  scott0  8196  hsmex2  8705  iooval2  11436  fzval2  11543  hashbc  12310  dfphi2  13953  phimullem  13958  mrcfval  14650  mrisval  14672  ipoval  15428  pmtrfval  16060  psgnfval  16110  pmtrsn  16129  lspfval  17162  lsppropd  17207  rrgval  17466  aspval  17507  psrval  17537  mvrfval  17602  ltbval  17662  opsrval  17665  dsmmbas2  18273  dsmmelbas  18275  frlmbas  18291  frlmbasOLD  18292  m1detdiag  18521  clsfval  18747  ordtrest  18924  ordtrest2lem  18925  ordtrest2  18926  xkoval  19278  xkopt  19346  qtopres  19389  kqval  19417  tsmsval2  19818  cncfval  20582  isphtpy  20671  cfilfval  20893  iscmet  20913  ttgval  23258  eengv  23362  isumgra  23386  isuslgra  23408  isusgra  23409  ordtprsval  26484  ordtrestNEW  26487  ordtrest2NEWlem  26488  omsval  26844  orrvcval4  26983  orrvcoel  26984  orrvccel  26985  snmlfval  27355  funray  28307  fvray  28308  itg2addnclem2  28584  isptfin  28707  islocfin  28708  cntotbnd  28835  pellfundval  29361  elmnc  29633  rgspnval  29665  elfvmptrab  30295  elovmpt2wrd  30396  wwlkn  30456  clwwlkn  30570  clwwlknprop  30575  hashecclwwlkn1  30648  usghashecclwwlk  30649  rusgrasn  30697  numclwwlkovf2  30817  numclwwlkqhash  30833  rmsuppss  30923  mndpsuppss  30924  scmsuppss  30925  docaffvalN  35074  docafvalN  35075  lcfr  35538  hlhilocv  35913