Theorem rabeqbidv 2911

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 2910	. . 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 2908	. 2 |- ( ph -> { x e. B | ps } = { x e. B | ch } )
6	3, 5	eqtrd 2436	1 |- ( ph -> { x e. A | ps } = { x e. B | ch } )

Syntax hints:   -> wi 4   <-> wb 177   = wceq 1649   {crab 2670

This theorem is referenced by:  mpt2xopoveq  6429  phival  13111  dfphi2  13118  hashbcval  13325  imasval  13692  ismre  13770  mrisval  13810  isacs  13831  monfval  13913  ismon  13914  monpropd  13918  natfval  14098  isnat  14099  coafval  14174  ismhm  14695  issubm  14703  gsumvalx  14729  gsumpropd  14731  gsumress  14732  issubg  14899  isnsg  14924  isgim  15004  isga  15023  cntzfval  15074  isslw  15197  dprdval  15516  isirred  15759  dfrhm2  15776  issubrg  15823  abvfval  15861  lssset  15965  islmhm  16058  islmim  16089  islbs  16103  rrgval  16302  mplval  16447  mplbaspropd  16585  ocvfval  16848  isobs  16902  cldval  17042  mretopd  17111  neifval  17118  ordtval  17207  ordtbas2  17209  ordtcnv  17219  ordtrest2  17222  cnfval  17251  cnpfval  17252  kgenval  17520  xkoval  17572  dfac14  17603  qtopval  17680  qtopval2  17681  hmeofval  17743  elmptrab  17812  fgval  17855  flimval  17948  utopval  18215  ucnval  18260  iscfilu  18271  ispsmet  18288  ismet  18306  isxmet  18307  blfvalps  18366  cncfval  18871  ishtpy  18950  isphtpy  18959  om1val  19008  cfilfval  19170  caufval  19181  cpnfval  19771  uc1pval  20015  mon1pval  20017  dchrval  20971  isausgra  21332  usgraeq12d  21338  usgra0v  21344  usgra1v  21362  nbgraop  21389  isuvtx  21450  vdgrfval  21619  lnoval  22206  bloval  22235  hmoval  22264  sigagenval  24476  faeval  24550  ismbfm  24555  sitgval  24600  erdszelem3  24832  erdsze  24841  kur14  24855  iscvm  24899  elgiso  25060  istotbnd  26368  isbnd  26379  rngohomval  26470  rngoisoval  26483  idlval  26513  pridlval  26533  maxidlval  26539  igenval  26561  isnacs  26648  mzpclval  26672  supeq123d  27026  dsmmval  27068  islinds  27147  issdrg  27373  is2wlkonot  28060  is2spthonot  28061  2wlksot  28064  2spthsot  28065  2wlkonot3v  28072  2spthonot3v  28073  lshpset  29461  lflset  29542  pats  29768  llnset  29987  lplnset  30011  lvolset  30054  lineset  30220  pmapfval  30238  paddfval  30279  pclfvalN  30371  lhpset  30477  ldilfset  30590  ltrnfset  30599  ltrnset  30600  dilfsetN  30634  trnfsetN  30637  trnsetN  30638  diaffval  31513  diafval  31514  dicffval  31657  dochffval  31832  lpolsetN  31965  lcdfval  32071  lcdval  32072  mapdffval  32109  mapdfval  32110

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rab 2675