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

Theorem rabbidv 2793
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 451 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
32rabbidva 2792 1  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  A  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632    e. wcel 1696   {crab 2560
This theorem is referenced by:  rabeqbidv  2796  difeq2  3301  seex  4372  mptiniseg  5183  fineqvlem  7093  supeq1  7214  supeq2  7217  oieq1  7243  oieq2  7244  ordtypecbv  7248  ordtypelem3  7251  harval  7292  inf3lema  7341  wemapwe  7416  oef1o  7417  tz9.12lem3  7477  rankvalb  7485  rankvalg  7505  ranksnb  7515  rankonidlem  7516  cardval3  7601  cardidm  7608  alephsuc2  7723  coftr  7915  fin1a2lem11  8052  fin1a2lem12  8053  hsmex  8074  axdc3lem2  8093  zorn2lem1  8139  zorn2lem6  8144  zorn2lem7  8145  zorn2g  8146  wuncval  8380  tskmval  8477  peano5uzti  10117  uzval  10248  reexALT  10364  ixxval  10680  fzval  10800  hashbclem  11406  hashbc  11407  shftfn  11584  rpnnen  12521  bitsfval  12630  sadfval  12659  sadcom  12670  smufval  12684  smupp1  12687  smupval  12695  smumullem  12699  gcdval  12703  bezoutlem2  12734  bezoutlem4  12736  isprm  12776  isprm2lem  12781  odzval  12872  pcval  12913  pceulem  12914  pceu  12915  pczpre  12916  pcdiv  12921  prmreclem1  12979  prmreclem4  12982  prmreclem5  12983  ramval  13071  imasdsval  13434  mrcval  13528  eldmcoa  13913  cycsubg2  14670  cntzval  14813  cntzsnval  14816  odfval  14864  odval  14865  gexval  14905  efgsfo  15064  dprdval  15254  ablfac1a  15320  ablfac1b  15321  ablfac1eu  15324  ablfaclem1  15336  ablfaclem3  15338  lspval  15748  aspval  16084  psrass1lem  16139  psrmulval  16147  mplmonmul  16224  coe1mul2  16362  ocvval  16583  istopon  16679  clsval  16790  neival  16855  ordtbaslem  16934  ordtbas2  16937  ordtopn1  16940  ordtopn2  16941  cnpval  16982  llyeq  17212  nllyeq  17213  xkoopn  17300  kqfval  17430  tsmsfbas  17826  blval  17964  nmofval  18239  nmoval  18240  ishtpy  18486  minveclem3b  18808  minveclem3  18809  minveclem4  18812  minveclem5  18813  ovolval  18849  vitalilem2  18980  vitalilem3  18981  vitalilem4  18982  vitali  18984  itg2monolem1  19121  elcpn  19299  mdegmullem  19480  elqaalem1  19715  elqaalem2  19716  elqaalem3  19717  elqaa  19718  aannenlem1  19724  aannenlem2  19725  jensen  20299  vmaval  20367  muval  20386  sgmval  20396  fsumdvdscom  20441  musum  20447  muinv  20449  dchrisum0fval  20670  dchrisum0ff  20672  logsqvma2  20708  pntrlog2bndlem1  20742  sspval  21315  ubthlem1  21465  ubthlem2  21466  ubthlem3  21467  ocval  21875  spanval  21928  chsupid  22007  eigvecval  22492  specval  22494  ballotlemi  23075  measvuni  23557  orvcelval  23684  subfacp1lem6  23731  kur14  23762  cvmscbv  23804  cvmsi  23811  cvmsval  23812  vdgrval  23905  eupath2  23919  snmlval  23929  snmlflim  23930  fvray  24836  ubos  25359  istopx  25650  istopxc  25651  ishomb  25891  cinvlem2  25932  sgplpte21  26235  sgplpte22  26241  isray2  26256  ptfinfin  26401  finlocfin  26402  locfindis  26408  neibastop3  26414  2rexfrabdioph  26980  3rexfrabdioph  26981  4rexfrabdioph  26982  6rexfrabdioph  26983  7rexfrabdioph  26984  eldioph4i  26998  diophren  26999  pell1qrval  27034  pell14qrval  27036  pell1234qrval  27038  rpnnen3  27228  fnwe2lem1  27250  pwssplit4  27294  pwslnmlem2  27298  dsmmelbas  27308  frlmsslss  27347  mapfien2  27361  dgraaval  27452  itgoval  27469  rgspnval  27476  proot1hash  27622  stoweidlem26  27878  stoweidlem27  27879  stoweidlem34  27886  stoweidlem46  27898  bnj602  29263  islinei  30551  pmapval  30568  paddval  30609  paddcom  30624  pclvalN  30701  ldilset  30920  dilsetN  30964  diafval  31843  diaval  31844  docavalN  31935  dicfval  31987  dochfval  32162  dochval  32163  mapdval  32440  mapdsn2  32454
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-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-ral 2561  df-rab 2565
  Copyright terms: Public domain W3C validator