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

Theorem rabeqbidv 3042
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 3040 . . 3  |-  ( A  =  B  ->  { x  e.  A  |  ps }  =  { x  e.  B  |  ps } )
31, 2syl 17 . 2  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  B  |  ps } )
4 rabeqbidv.2 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
54rabbidv 3038 . 2  |-  ( ph  ->  { x  e.  B  |  ps }  =  {
x  e.  B  |  ch } )
63, 5eqtrd 2487 1  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  B  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1446   {crab 2743
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ral 2744  df-rab 2748
This theorem is referenced by:  elfvmptrab1  5975  elovmpt2rab1  6521  ovmpt3rab1  6530  suppval  6921  mpt2xopoveq  6970  supeq123d  7969  phival  14727  dfphi2  14734  hashbcval  14966  imasval  15423  imasvalOLD  15424  ismre  15508  mrisval  15548  isacs  15569  monfval  15649  ismon  15650  monpropd  15654  natfval  15863  isnat  15864  initoval  15904  termoval  15905  gsumvalx  16525  gsumpropd  16527  gsumress  16531  ismhm  16596  issubm  16606  issubg  16829  isnsg  16858  isgim  16938  isga  16957  cntzfval  16986  isslw  17272  isirred  17939  dfrhm2  17957  isrim0  17963  issubrg  18020  abvfval  18058  lssset  18169  islmhm  18262  islmim  18297  islbs  18311  rrgval  18523  mplval  18664  mplbaspropd  18842  ocvfval  19241  isobs  19295  dsmmval  19309  islinds  19379  dmatval  19529  scmatval  19541  cpmat  19745  cldval  20050  mretopd  20120  neifval  20127  ordtval  20217  ordtbas2  20219  ordtcnv  20229  ordtrest2  20232  cnfval  20261  cnpfval  20262  kgenval  20562  xkoval  20614  dfac14  20645  qtopval  20722  qtopval2  20723  hmeofval  20785  elmptrab  20854  fgval  20897  flimval  20990  utopval  21259  ucnval  21304  iscfilu  21315  ispsmet  21332  ismet  21350  isxmet  21351  blfvalps  21410  cncfval  21932  ishtpy  22015  isphtpy  22024  om1val  22073  cfilfval  22246  caufval  22257  cpnfval  22898  uc1pval  23102  mon1pval  23104  dchrval  24174  istrkgl  24518  israg  24754  iseqlg  24909  ttgval  24917  nbgraop  25163  isuvtx  25228  wwlk  25421  clwwlk  25506  is2wlkonot  25603  is2spthonot  25604  2wlksot  25607  2spthsot  25608  2wlkonot3v  25615  2spthonot3v  25616  vdgrfval  25635  rusgranumwlklem2  25690  numclwwlkovf  25821  numclwwlkovg  25827  numclwwlkovq  25839  numclwwlkovh  25841  numclwwlk5  25852  lnoval  26405  bloval  26434  hmoval  26463  ordtprsuni  28737  sigagenval  28974  faeval  29081  ismbfm  29086  carsgval  29147  sitgval  29177  erdszelem3  29928  erdsze  29937  kur14  29951  iscvm  29994  elgiso  30326  wlimeq12  30514  fwddifval  30941  poimirlem28  31980  istotbnd  32113  isbnd  32124  rngohomval  32215  rngoisoval  32228  idlval  32258  pridlval  32278  maxidlval  32284  igenval  32306  lshpset  32556  lflset  32637  pats  32863  llnset  33082  lplnset  33106  lvolset  33149  lineset  33315  pmapfval  33333  paddfval  33374  lhpset  33572  ldilfset  33685  ltrnfset  33694  ltrnset  33695  dilfsetN  33730  trnfsetN  33733  trnsetN  33734  diaffval  34610  diafval  34611  dicffval  34754  dochffval  34929  lpolsetN  35062  lcdfval  35168  lcdval  35169  mapdffval  35206  mapdfval  35207  isnacs  35558  mzpclval  35579  issdrg  36075  fourierdlem2  37981  fourierdlem3  37982  etransclem12  38121  etransclem33  38142  caragenval  38324  iccpval  38739  nbgrval  39416  uvtxaval  39469  vtxdgfval  39538  umgr2v2evd2  39574  ismgmhm  39887  issubmgm  39893  assintopval  39945  rnghmval  39995  isrngisom  40000  dmatALTval  40297  lcoop  40308
  Copyright terms: Public domain W3C validator