Theorem rabeqbidv 3090

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

Syntax hints:   -> wi 4   <-> wb 184   = 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-ral 2798  df-rab 2802

This theorem is referenced by:  elfvmptrab1  5961  elovmpt2rab1  6507  ovmpt3rab1  6519  suppval  6905  mpt2xopoveq  6949  supeq123d  7912  phival  14279  dfphi2  14286  hashbcval  14502  imasval  14890  ismre  14969  mrisval  15009  isacs  15030  monfval  15109  ismon  15110  monpropd  15114  natfval  15294  isnat  15295  coafval  15370  gsumvalx  15876  gsumpropd  15878  gsumress  15882  ismhm  15947  issubm  15957  issubg  16180  isnsg  16209  isgim  16289  isga  16308  cntzfval  16337  isslw  16607  dprdval  17013  dprdvalOLD  17015  isirred  17327  dfrhm2  17345  isrim0  17351  issubrg  17408  abvfval  17446  lssset  17559  islmhm  17652  islmim  17687  islbs  17701  rrgval  17914  mplval  18063  mplbaspropd  18257  ocvfval  18675  isobs  18729  dsmmval  18743  islinds  18822  dmatval  18972  scmatval  18984  cpmat  19188  cldval  19502  mretopd  19571  neifval  19578  ordtval  19668  ordtbas2  19670  ordtcnv  19680  ordtrest2  19683  cnfval  19712  cnpfval  19713  kgenval  20014  xkoval  20066  dfac14  20097  qtopval  20174  qtopval2  20175  hmeofval  20237  elmptrab  20306  fgval  20349  flimval  20442  utopval  20713  ucnval  20758  iscfilu  20769  ispsmet  20786  ismet  20804  isxmet  20805  blfvalps  20864  cncfval  21370  ishtpy  21450  isphtpy  21459  om1val  21508  cfilfval  21681  caufval  21692  cpnfval  22313  uc1pval  22518  mon1pval  22520  dchrval  23487  istrkgl  23833  israg  24052  ttgval  24156  isausgra  24332  usgraeq12d  24340  usgra0v  24349  usgra1v  24368  nbgraop  24401  isuvtx  24466  wwlk  24659  clwwlk  24744  is2wlkonot  24841  is2spthonot  24842  2wlksot  24845  2spthsot  24846  2wlkonot3v  24853  2spthonot3v  24854  vdgrfval  24873  rusgranumwlklem2  24928  numclwwlkovf  25059  numclwwlkovg  25065  numclwwlkovq  25077  numclwwlkovh  25079  numclwwlk5  25090  lnoval  25645  bloval  25674  hmoval  25703  ordtprsuni  27879  sigagenval  28118  faeval  28196  ismbfm  28201  sitgval  28252  erdszelem3  28615  erdsze  28624  kur14  28638  iscvm  28682  mpstval  28873  elgiso  29014  wlimeq12  29351  istotbnd  30241  isbnd  30252  rngohomval  30343  rngoisoval  30356  idlval  30386  pridlval  30406  maxidlval  30412  igenval  30434  isnacs  30612  mzpclval  30633  issdrg  31122  fourierdlem2  31845  fourierdlem3  31846  ismgmhm  32425  issubmgm  32431  assintopval  32482  rnghmval  32532  isrngisom  32537  dmatALTval  32871  lcoop  32882  lshpset  34578  lflset  34659  pats  34885  llnset  35104  lplnset  35128  lvolset  35171  lineset  35337  pmapfval  35355  paddfval  35396  pclfvalN  35488  lhpset  35594  ldilfset  35707  ltrnfset  35716  ltrnset  35717  dilfsetN  35752  trnfsetN  35755  trnsetN  35756  diaffval  36632  diafval  36633  dicffval  36776  dochffval  36951  lpolsetN  37084  lcdfval  37190  lcdval  37191  mapdffval  37228  mapdfval  37229