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

Theorem rabbidv 2957
Description: Equivalent wff's yield equal restricted class abstractions (deduction rule). (Contributed by NM, 10-Feb-1995.)
Hypothesis
Ref Expression
rabbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
rabbidv  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  A  |  ch } )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem rabbidv
StepHypRef Expression
1 rabbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21adantr 453 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
32rabbidva 2956 1  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  A  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1654    e. wcel 1728   {crab 2716
This theorem is referenced by:  rabeqbidv  2960  difeq2  3448  seex  4580  mptiniseg  5399  fineqvlem  7359  supeq1  7486  supeq2  7489  supeq3  7490  oieq1  7517  oieq2  7518  ordtypecbv  7522  ordtypelem3  7525  harval  7566  inf3lema  7615  wemapwe  7690  oef1o  7691  tz9.12lem3  7751  rankvalb  7759  rankvalg  7779  ranksnb  7789  rankonidlem  7790  cardval3  7877  cardidm  7884  alephsuc2  7999  coftr  8191  fin1a2lem11  8328  fin1a2lem12  8329  hsmex  8350  axdc3lem2  8369  zorn2lem1  8414  zorn2lem6  8419  zorn2lem7  8420  zorn2g  8421  wuncval  8655  tskmval  8752  peano5uzti  10397  uzval  10528  reexALT  10644  ixxval  10962  fzval  11083  hashbclem  11739  hashbc  11740  shftfn  11926  rpnnen  12864  bitsfval  12973  sadfval  13002  sadcom  13013  smufval  13027  smupp1  13030  smupval  13038  smumullem  13042  gcdval  13046  bezoutlem2  13077  bezoutlem4  13079  isprm  13119  isprm2lem  13124  odzval  13215  pcval  13256  pceulem  13257  pceu  13258  pczpre  13259  pcdiv  13264  prmreclem1  13322  prmreclem4  13325  prmreclem5  13326  ramval  13414  imasdsval  13779  mrcval  13873  eldmcoa  14258  cycsubg2  15015  cntzval  15158  cntzsnval  15161  odfval  15209  odval  15210  gexval  15250  efgsfo  15409  dprdval  15599  ablfac1a  15665  ablfac1b  15666  ablfac1eu  15669  ablfaclem1  15681  ablfaclem3  15683  lspval  16089  aspval  16425  psrass1lem  16480  psrmulval  16488  mplmonmul  16565  coe1mul2  16700  ocvval  16932  istopon  17028  clsval  17139  neival  17204  ordtbaslem  17290  ordtbas2  17293  ordtopn1  17296  ordtopn2  17297  cnpval  17338  llyeq  17571  nllyeq  17572  xkoopn  17659  kqfval  17793  tsmsfbas  18195  blvalps  18453  blval  18454  nmofval  18786  nmoval  18787  ishtpy  19035  minveclem3b  19367  minveclem3  19368  minveclem4  19371  minveclem5  19372  ovolval  19408  vitalilem2  19539  vitalilem3  19540  vitalilem4  19541  vitali  19543  itg2monolem1  19678  elcpn  19858  mdegmullem  20039  elqaalem1  20274  elqaalem2  20275  elqaalem3  20276  elqaa  20277  aannenlem1  20283  aannenlem2  20284  jensen  20865  vmaval  20934  muval  20953  sgmval  20963  fsumdvdscom  21008  musum  21014  muinv  21016  dchrisum0fval  21237  dchrisum0ff  21239  logsqvma2  21275  pntrlog2bndlem1  21309  nbgraop1  21475  vdgrval  21705  eupath2  21740  sspval  22260  ubthlem1  22410  ubthlem2  22411  ubthlem3  22412  ocval  22820  spanval  22873  chsupid  22952  eigvecval  23437  specval  23439  measvuni  24603  brfae  24634  orvcelval  24761  ballotlemi  24793  subfacp1lem6  24906  kur14  24937  cvmscbv  24980  cvmsi  24987  cvmsval  24988  snmlval  25053  snmlflim  25054  dfpred3g  25485  fvray  26110  ftc1anclem6  26327  ptfinfin  26420  finlocfin  26421  locfindis  26427  neibastop3  26433  2rexfrabdioph  26968  3rexfrabdioph  26969  4rexfrabdioph  26970  6rexfrabdioph  26971  7rexfrabdioph  26972  eldioph4i  26985  diophren  26986  pell1qrval  27021  pell14qrval  27023  pell1234qrval  27025  rpnnen3  27215  fnwe2lem1  27237  pwssplit4  27280  pwslnmlem2  27284  dsmmelbas  27294  frlmsslss  27333  mapfien2  27347  dgraaval  27438  itgoval  27455  rgspnval  27462  proot1hash  27608  stoweidlem26  27863  stoweidlem27  27864  stoweidlem31  27868  stoweidlem34  27871  stoweidlem46  27883  elovmpt2rab  28202  elovmpt3rab1  28205  wwlkn  28462  2wlkonot  28495  2spthonot  28496  usg2spot2nb  28626  usgreg2spot  28628  2spotmdisj  28629  usgreghash2spot  28630  bnj602  29460  islinei  30711  pmapval  30728  paddval  30769  paddcom  30784  pclvalN  30861  ldilset  31080  dilsetN  31124  diafval  32003  diaval  32004  docavalN  32095  dicfval  32147  dochfval  32322  dochval  32323  mapdval  32600  mapdsn2  32614
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-ral 2717  df-rab 2721
  Copyright terms: Public domain W3C validator