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

Theorem rabeqbidv 2953
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 2952 . . 3  |-  ( A  =  B  ->  { x  e.  A  |  ps }  =  { x  e.  B  |  ps } )
31, 2syl 16 . 2  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  B  |  ps } )
4 rabeqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
54rabbidv 2950 . 2  |-  ( ph  ->  { x  e.  B  |  ps }  =  {
x  e.  B  |  ch } )
63, 5eqtrd 2470 1  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  B  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653   {crab 2711
This theorem is referenced by:  mpt2xopoveq  6472  supeq123d  7457  phival  13158  dfphi2  13165  hashbcval  13372  imasval  13739  ismre  13817  mrisval  13857  isacs  13878  monfval  13960  ismon  13961  monpropd  13965  natfval  14145  isnat  14146  coafval  14221  ismhm  14742  issubm  14750  gsumvalx  14776  gsumpropd  14778  gsumress  14779  issubg  14946  isnsg  14971  isgim  15051  isga  15070  cntzfval  15121  isslw  15244  dprdval  15563  isirred  15806  dfrhm2  15823  issubrg  15870  abvfval  15908  lssset  16012  islmhm  16105  islmim  16136  islbs  16150  rrgval  16349  mplval  16494  mplbaspropd  16632  ocvfval  16895  isobs  16949  cldval  17089  mretopd  17158  neifval  17165  ordtval  17255  ordtbas2  17257  ordtcnv  17267  ordtrest2  17270  cnfval  17299  cnpfval  17300  kgenval  17569  xkoval  17621  dfac14  17652  qtopval  17729  qtopval2  17730  hmeofval  17792  elmptrab  17861  fgval  17904  flimval  17997  utopval  18264  ucnval  18309  iscfilu  18320  ispsmet  18337  ismet  18355  isxmet  18356  blfvalps  18415  cncfval  18920  ishtpy  18999  isphtpy  19008  om1val  19057  cfilfval  19219  caufval  19230  cpnfval  19820  uc1pval  20064  mon1pval  20066  dchrval  21020  isausgra  21381  usgraeq12d  21387  usgra0v  21393  usgra1v  21411  nbgraop  21438  isuvtx  21499  vdgrfval  21668  lnoval  22255  bloval  22284  hmoval  22313  sigagenval  24525  faeval  24599  ismbfm  24604  sitgval  24649  erdszelem3  24881  erdsze  24890  kur14  24904  iscvm  24948  elgiso  25109  wlimeq12  25572  istotbnd  26480  isbnd  26491  rngohomval  26582  rngoisoval  26595  idlval  26625  pridlval  26645  maxidlval  26651  igenval  26673  isnacs  26760  mzpclval  26784  dsmmval  27179  islinds  27258  issdrg  27484  elovmpt2rab1  28093  ovmpt3rab1  28094  wwlk  28351  is2wlkonot  28383  is2spthonot  28384  2wlksot  28387  2spthsot  28388  2wlkonot3v  28395  2spthonot3v  28396  lshpset  29838  lflset  29919  pats  30145  llnset  30364  lplnset  30388  lvolset  30431  lineset  30597  pmapfval  30615  paddfval  30656  pclfvalN  30748  lhpset  30854  ldilfset  30967  ltrnfset  30976  ltrnset  30977  dilfsetN  31011  trnfsetN  31014  trnsetN  31015  diaffval  31890  diafval  31891  dicffval  32034  dochffval  32209  lpolsetN  32342  lcdfval  32448  lcdval  32449  mapdffval  32486  mapdfval  32487
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rab 2716
  Copyright terms: Public domain W3C validator