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

Theorem rabeqbidv 2796
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 2795 . . 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 2793 . 2  |-  ( ph  ->  { x  e.  B  |  ps }  =  {
x  e.  B  |  ch } )
63, 5eqtrd 2328 1  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  B  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632   {crab 2560
This theorem is referenced by:  phival  12851  dfphi2  12858  hashbcval  13065  imasval  13430  ismre  13508  mrisval  13548  isacs  13569  monfval  13651  ismon  13652  monpropd  13656  natfval  13836  isnat  13837  coafval  13912  ismhm  14433  issubm  14441  gsumvalx  14467  gsumpropd  14469  gsumress  14470  issubg  14637  isnsg  14662  isgim  14742  isga  14761  cntzfval  14812  isslw  14935  dprdval  15254  isirred  15497  dfrhm2  15514  issubrg  15561  abvfval  15599  lssset  15707  islmhm  15800  islmim  15831  islbs  15845  rrgval  16044  mplval  16189  mplbaspropd  16330  ocvfval  16582  isobs  16636  cldval  16776  mretopd  16845  neifval  16852  ordtval  16935  ordtbas2  16937  ordtcnv  16947  ordtrest2  16950  cnfval  16979  cnpfval  16980  kgenval  17246  xkoval  17298  dfac14  17328  qtopval  17402  qtopval2  17403  hmeofval  17465  elmptrab  17538  fgval  17581  flimval  17674  ismet  17904  isxmet  17905  blfval  17963  cncfval  18408  ishtpy  18486  isphtpy  18495  om1val  18544  cfilfval  18706  caufval  18717  cpnfval  19297  uc1pval  19541  mon1pval  19543  dchrval  20489  lnoval  21346  bloval  21375  hmoval  21404  sigagenval  23516  ismbfm  23572  erdszelem3  23739  erdsze  23748  kur14  23762  iscvm  23805  vdgrfval  23904  elgiso  24018  isorhom  25314  mxlelt  25367  mxlelt2  25368  mnlelt2  25369  mnlmxl2  25372  idlvalNEW  25548  ishoma  25890  ismona  25912  isepia  25922  isiso  25928  cinvlem1  25931  isfuna  25937  isinob  25965  issrc  25970  propsrc  25971  isntr  25976  islimcat  25979  isnword  26089  isconcl1b  26200  sgplpte21  26235  sgplpte22  26241  isray2  26256  isray  26257  rabeq12OLD  26453  istotbnd  26596  isbnd  26607  rngohomval  26698  rngoisoval  26711  idlval  26741  pridlval  26761  maxidlval  26767  igenval  26789  isnacs  26882  mzpclval  26906  supeq123d  27261  dsmmval  27303  islinds  27382  issdrg  27608  stoweidlem31  27883  stoweidlem34  27886  mpt2xopoveq  28201  usgraeq12d  28245  usgra0v  28251  usgra1v  28260  nbgraop  28274  isuvtx  28301  lshpset  29790  lflset  29871  pats  30097  llnset  30316  lplnset  30340  lvolset  30383  lineset  30549  pmapfval  30567  paddfval  30608  pclfvalN  30700  lhpset  30806  ldilfset  30919  ltrnfset  30928  ltrnset  30929  dilfsetN  30963  trnfsetN  30966  trnsetN  30967  diaffval  31842  diafval  31843  dicffval  31986  dochffval  32161  lpolsetN  32294  lcdfval  32400  lcdval  32401  mapdffval  32438  mapdfval  32439
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rab 2565
  Copyright terms: Public domain W3C validator