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

Theorem rabbidv 2916
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 452 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
32rabbidva 2915 1  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  A  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    e. wcel 1721   {crab 2678
This theorem is referenced by:  rabeqbidv  2919  difeq2  3427  seex  4513  mptiniseg  5331  fineqvlem  7290  supeq1  7416  supeq2  7419  oieq1  7445  oieq2  7446  ordtypecbv  7450  ordtypelem3  7453  harval  7494  inf3lema  7543  wemapwe  7618  oef1o  7619  tz9.12lem3  7679  rankvalb  7687  rankvalg  7707  ranksnb  7717  rankonidlem  7718  cardval3  7803  cardidm  7810  alephsuc2  7925  coftr  8117  fin1a2lem11  8254  fin1a2lem12  8255  hsmex  8276  axdc3lem2  8295  zorn2lem1  8340  zorn2lem6  8345  zorn2lem7  8346  zorn2g  8347  wuncval  8581  tskmval  8678  peano5uzti  10323  uzval  10454  reexALT  10570  ixxval  10888  fzval  11009  hashbclem  11664  hashbc  11665  shftfn  11851  rpnnen  12789  bitsfval  12898  sadfval  12927  sadcom  12938  smufval  12952  smupp1  12955  smupval  12963  smumullem  12967  gcdval  12971  bezoutlem2  13002  bezoutlem4  13004  isprm  13044  isprm2lem  13049  odzval  13140  pcval  13181  pceulem  13182  pceu  13183  pczpre  13184  pcdiv  13189  prmreclem1  13247  prmreclem4  13250  prmreclem5  13251  ramval  13339  imasdsval  13704  mrcval  13798  eldmcoa  14183  cycsubg2  14940  cntzval  15083  cntzsnval  15086  odfval  15134  odval  15135  gexval  15175  efgsfo  15334  dprdval  15524  ablfac1a  15590  ablfac1b  15591  ablfac1eu  15594  ablfaclem1  15606  ablfaclem3  15608  lspval  16014  aspval  16350  psrass1lem  16405  psrmulval  16413  mplmonmul  16490  coe1mul2  16625  ocvval  16857  istopon  16953  clsval  17064  neival  17129  ordtbaslem  17214  ordtbas2  17217  ordtopn1  17220  ordtopn2  17221  cnpval  17262  llyeq  17494  nllyeq  17495  xkoopn  17582  kqfval  17716  tsmsfbas  18118  blvalps  18376  blval  18377  nmofval  18709  nmoval  18710  ishtpy  18958  minveclem3b  19290  minveclem3  19291  minveclem4  19294  minveclem5  19295  ovolval  19331  vitalilem2  19462  vitalilem3  19463  vitalilem4  19464  vitali  19466  itg2monolem1  19603  elcpn  19781  mdegmullem  19962  elqaalem1  20197  elqaalem2  20198  elqaalem3  20199  elqaa  20200  aannenlem1  20206  aannenlem2  20207  jensen  20788  vmaval  20857  muval  20876  sgmval  20886  fsumdvdscom  20931  musum  20937  muinv  20939  dchrisum0fval  21160  dchrisum0ff  21162  logsqvma2  21198  pntrlog2bndlem1  21232  nbgraop1  21398  vdgrval  21628  eupath2  21663  sspval  22183  ubthlem1  22333  ubthlem2  22334  ubthlem3  22335  ocval  22743  spanval  22796  chsupid  22875  eigvecval  23360  specval  23362  measvuni  24529  brfae  24560  orvcelval  24687  ballotlemi  24719  subfacp1lem6  24832  kur14  24863  cvmscbv  24906  cvmsi  24913  cvmsval  24914  snmlval  24979  snmlflim  24980  fvray  25987  ptfinfin  26276  finlocfin  26277  locfindis  26283  neibastop3  26289  2rexfrabdioph  26754  3rexfrabdioph  26755  4rexfrabdioph  26756  6rexfrabdioph  26757  7rexfrabdioph  26758  eldioph4i  26771  diophren  26772  pell1qrval  26807  pell14qrval  26809  pell1234qrval  26811  rpnnen3  27001  fnwe2lem1  27023  pwssplit4  27067  pwslnmlem2  27071  dsmmelbas  27081  frlmsslss  27120  mapfien2  27134  dgraaval  27225  itgoval  27242  rgspnval  27249  proot1hash  27395  stoweidlem26  27650  stoweidlem27  27651  stoweidlem31  27655  stoweidlem34  27658  stoweidlem46  27670  2wlkonot  28070  2spthonot  28071  usg2spot2nb  28176  usgreg2spot  28178  2spotmdisj  28179  usgreghash2spot  28180  bnj602  29004  islinei  30234  pmapval  30251  paddval  30292  paddcom  30307  pclvalN  30384  ldilset  30603  dilsetN  30647  diafval  31526  diaval  31527  docavalN  31618  dicfval  31670  dochfval  31845  dochval  31846  mapdval  32123  mapdsn2  32137
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-ral 2679  df-rab 2683
  Copyright terms: Public domain W3C validator