Theorem rabeq 3089

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

Syntax hints:   -> wi 4   = wceq 1383   {crab 2797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802

This theorem is referenced by:  rabeqbidv  3090  rabeqbidva  3091  difeq1  3600  ifeq1  3930  ifeq2  3931  rabsnif  4084  elfvmptrab  5962  supp0  6908  suppvalfn  6910  suppsnop  6917  fnsuppres  6929  pmvalg  7433  supeq2  7910  oieq2  7941  cantnffval  8083  scott0  8307  hsmex2  8816  iooval2  11571  fzval2  11684  hashbc  12481  elovmpt2wrd  12562  dfphi2  14181  phimullem  14186  mrcfval  14882  mrisval  14904  ipoval  15658  pmtrfval  16349  psgnfval  16399  pmtrsn  16418  lspfval  17493  lsppropd  17538  rrgval  17809  aspval  17851  psrval  17885  mvrfval  17950  ltbval  18010  opsrval  18013  dsmmbas2  18641  dsmmelbas  18643  frlmbas  18659  frlmbasOLD  18660  m1detdiag  18972  clsfval  19399  ordtrest  19576  ordtrest2lem  19577  ordtrest2  19578  isptfin  19890  islocfin  19891  xkoval  19961  xkopt  20029  qtopres  20072  kqval  20100  tsmsval2  20501  cncfval  21265  isphtpy  21354  cfilfval  21576  iscmet  21596  ttgval  24050  eengv  24154  isumgra  24187  isuslgra  24215  isusgra  24216  edgss  24224  wwlkn  24554  clwwlkn  24639  clwwlknprop  24644  hashecclwwlkn1  24706  usghashecclwwlk  24707  rusgrasn  24817  numclwwlkovf2  24956  numclwwlkqhash  24972  ordtprsval  27773  ordtrestNEW  27776  ordtrest2NEWlem  27777  omsval  28137  orrvcval4  28276  orrvcoel  28277  orrvccel  28278  snmlfval  28648  funray  29765  fvray  29766  itg2addnclem2  30042  cntotbnd  30267  pellfundval  30791  elmnc  31061  rgspnval  31093  isfusgra  32262  usgfis  32284  usgfisALT  32288  assintopmap  32367  rmsuppss  32698  mndpsuppss  32699  scmsuppss  32700  dmatALTval  32736  dmatALTbas  32737  docaffvalN  36588  docafvalN  36589  lcfr  37052  hlhilocv  37427