MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rabeqbidv Unicode version

Theorem rabeqbidv 2783
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
StepHypRef Expression
1 rabeqbidv.1 . . 3  |-  ( ph  ->  A  =  B )
2 rabeq 2782 . . 3  |-  ( A  =  B  ->  { x  e.  A  |  ps }  =  { x  e.  B  |  ps } )
31, 2syl 15 . 2  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  B  |  ps } )
4 rabeqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
54rabbidv 2780 . 2  |-  ( ph  ->  { x  e.  B  |  ps }  =  {
x  e.  B  |  ch } )
63, 5eqtrd 2315 1  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  B  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   {crab 2547
This theorem is referenced by:  phival  12835  dfphi2  12842  hashbcval  13049  imasval  13414  ismre  13492  mrisval  13532  isacs  13553  monfval  13635  ismon  13636  monpropd  13640  natfval  13820  isnat  13821  coafval  13896  ismhm  14417  issubm  14425  gsumvalx  14451  gsumpropd  14453  gsumress  14454  issubg  14621  isnsg  14646  isgim  14726  isga  14745  cntzfval  14796  isslw  14919  dprdval  15238  isirred  15481  dfrhm2  15498  issubrg  15545  abvfval  15583  lssset  15691  islmhm  15784  islmim  15815  islbs  15829  rrgval  16028  mplval  16173  mplbaspropd  16314  ocvfval  16566  isobs  16620  cldval  16760  mretopd  16829  neifval  16836  ordtval  16919  ordtbas2  16921  ordtcnv  16931  ordtrest2  16934  cnfval  16963  cnpfval  16964  kgenval  17230  xkoval  17282  dfac14  17312  qtopval  17386  qtopval2  17387  hmeofval  17449  elmptrab  17522  fgval  17565  flimval  17658  ismet  17888  isxmet  17889  blfval  17947  cncfval  18392  ishtpy  18470  isphtpy  18479  om1val  18528  cfilfval  18690  caufval  18701  cpnfval  19281  uc1pval  19525  mon1pval  19527  dchrval  20473  lnoval  21330  bloval  21359  hmoval  21388  sigagenval  23501  ismbfm  23557  erdszelem3  23724  erdsze  23733  kur14  23747  iscvm  23790  vdgrfval  23889  elgiso  24003  isorhom  25211  mxlelt  25264  mxlelt2  25265  mnlelt2  25266  mnlmxl2  25269  idlvalNEW  25445  ishoma  25787  ismona  25809  isepia  25819  isiso  25825  cinvlem1  25828  isfuna  25834  isinob  25862  issrc  25867  propsrc  25868  isntr  25873  islimcat  25876  isnword  25986  isconcl1b  26097  sgplpte21  26132  sgplpte22  26138  isray2  26153  isray  26154  rabeq12OLD  26350  istotbnd  26493  isbnd  26504  rngohomval  26595  rngoisoval  26608  idlval  26638  pridlval  26658  maxidlval  26664  igenval  26686  isnacs  26779  mzpclval  26803  supeq123d  27158  dsmmval  27200  islinds  27279  issdrg  27505  stoweidlem31  27780  stoweidlem34  27783  mpt2xopoveq  28085  usgraeq12d  28111  usgra0v  28117  usgra1v  28126  nbgraop  28140  isuvtx  28160  lshpset  29168  lflset  29249  pats  29475  llnset  29694  lplnset  29718  lvolset  29761  lineset  29927  pmapfval  29945  paddfval  29986  pclfvalN  30078  lhpset  30184  ldilfset  30297  ltrnfset  30306  ltrnset  30307  dilfsetN  30341  trnfsetN  30344  trnsetN  30345  diaffval  31220  diafval  31221  dicffval  31364  dochffval  31539  lpolsetN  31672  lcdfval  31778  lcdval  31779  mapdffval  31816  mapdfval  31817
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rab 2552
  Copyright terms: Public domain W3C validator