Theorem rabeqbidv 3029

Description: Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.)

Hypotheses

Ref	Expression
rabeqbidv.1	|- ( ph -> A = B )
rabeqbidv.2	|- ( ph -> ( ps <-> ch ) )

Assertion

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

Distinct variable groups:   x, A   x, B   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem rabeqbidv

Step	Hyp	Ref	Expression
1		rabeqbidv.1	. . 3 |- ( ph -> A = B )
2		rabeq 3028	. . 3 |- ( A = B -> { x e. A | ps } = { x e. B | ps } )
3	1, 2	syl 16	. 2 |- ( ph -> { x e. A | ps } = { x e. B | ps } )
4		rabeqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
5	4	rabbidv 3026	. 2 |- ( ph -> { x e. B | ps } = { x e. B | ch } )
6	3, 5	eqtrd 2423	1 |- ( ph -> { x e. A | ps } = { x e. B | ch } )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1399   {crab 2736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ral 2737  df-rab 2741

This theorem is referenced by:  elfvmptrab1  5878  elovmpt2rab1  6421  ovmpt3rab1  6433  suppval  6819  mpt2xopoveq  6865  supeq123d  7824  phival  14299  dfphi2  14306  hashbcval  14522  imasval  14918  ismre  14997  mrisval  15037  isacs  15058  monfval  15138  ismon  15139  monpropd  15143  natfval  15352  isnat  15353  initoval  15393  termoval  15394  coafval  15460  gsumvalx  16014  gsumpropd  16016  gsumress  16020  ismhm  16085  issubm  16095  issubg  16318  isnsg  16347  isgim  16427  isga  16446  cntzfval  16475  isslw  16745  dprdval  17147  dprdvalOLD  17149  isirred  17461  dfrhm2  17479  isrim0  17485  issubrg  17542  abvfval  17580  lssset  17693  islmhm  17786  islmim  17821  islbs  17835  rrgval  18048  mplval  18197  mplbaspropd  18391  ocvfval  18788  isobs  18842  dsmmval  18856  islinds  18929  dmatval  19079  scmatval  19091  cpmat  19295  cldval  19609  mretopd  19679  neifval  19686  ordtval  19776  ordtbas2  19778  ordtcnv  19788  ordtrest2  19791  cnfval  19820  cnpfval  19821  kgenval  20121  xkoval  20173  dfac14  20204  qtopval  20281  qtopval2  20282  hmeofval  20344  elmptrab  20413  fgval  20456  flimval  20549  utopval  20820  ucnval  20865  iscfilu  20876  ispsmet  20893  ismet  20911  isxmet  20912  blfvalps  20971  cncfval  21477  ishtpy  21557  isphtpy  21566  om1val  21615  cfilfval  21788  caufval  21799  cpnfval  22420  uc1pval  22625  mon1pval  22627  dchrval  23626  istrkgl  23972  israg  24194  ttgval  24299  isausgra  24475  usgraeq12d  24483  usgra0v  24492  usgra1v  24511  nbgraop  24544  isuvtx  24609  wwlk  24802  clwwlk  24887  is2wlkonot  24984  is2spthonot  24985  2wlksot  24988  2spthsot  24989  2wlkonot3v  24996  2spthonot3v  24997  vdgrfval  25016  rusgranumwlklem2  25071  numclwwlkovf  25202  numclwwlkovg  25208  numclwwlkovq  25220  numclwwlkovh  25222  numclwwlk5  25233  lnoval  25784  bloval  25813  hmoval  25842  ordtprsuni  28055  sigagenval  28289  faeval  28374  ismbfm  28379  carsgval  28430  sitgval  28457  erdszelem3  28826  erdsze  28835  kur14  28849  iscvm  28893  mpstval  29084  elgiso  29225  wlimeq12  29540  istotbnd  30431  isbnd  30442  rngohomval  30533  rngoisoval  30546  idlval  30576  pridlval  30596  maxidlval  30602  igenval  30624  isnacs  30802  mzpclval  30823  issdrg  31314  fourierdlem2  32057  fourierdlem3  32058  etransclem12  32195  etransclem33  32216  ismgmhm  32789  issubmgm  32795  assintopval  32847  rnghmval  32897  isrngisom  32902  dmatALTval  33201  lcoop  33212  lshpset  35116  lflset  35197  pats  35423  llnset  35642  lplnset  35666  lvolset  35709  lineset  35875  pmapfval  35893  paddfval  35934  pclfvalN  36026  lhpset  36132  ldilfset  36245  ltrnfset  36254  ltrnset  36255  dilfsetN  36290  trnfsetN  36293  trnsetN  36294  diaffval  37170  diafval  37171  dicffval  37314  dochffval  37489  lpolsetN  37622  lcdfval  37728  lcdval  37729  mapdffval  37766  mapdfval  37767