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

Theorem rabbidv 2948
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 2947 1  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  A  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725   {crab 2709
This theorem is referenced by:  rabeqbidv  2951  difeq2  3459  seex  4545  mptiniseg  5364  fineqvlem  7323  supeq1  7450  supeq2  7453  supeq3  7454  oieq1  7481  oieq2  7482  ordtypecbv  7486  ordtypelem3  7489  harval  7530  inf3lema  7579  wemapwe  7654  oef1o  7655  tz9.12lem3  7715  rankvalb  7723  rankvalg  7743  ranksnb  7753  rankonidlem  7754  cardval3  7839  cardidm  7846  alephsuc2  7961  coftr  8153  fin1a2lem11  8290  fin1a2lem12  8291  hsmex  8312  axdc3lem2  8331  zorn2lem1  8376  zorn2lem6  8381  zorn2lem7  8382  zorn2g  8383  wuncval  8617  tskmval  8714  peano5uzti  10359  uzval  10490  reexALT  10606  ixxval  10924  fzval  11045  hashbclem  11701  hashbc  11702  shftfn  11888  rpnnen  12826  bitsfval  12935  sadfval  12964  sadcom  12975  smufval  12989  smupp1  12992  smupval  13000  smumullem  13004  gcdval  13008  bezoutlem2  13039  bezoutlem4  13041  isprm  13081  isprm2lem  13086  odzval  13177  pcval  13218  pceulem  13219  pceu  13220  pczpre  13221  pcdiv  13226  prmreclem1  13284  prmreclem4  13287  prmreclem5  13288  ramval  13376  imasdsval  13741  mrcval  13835  eldmcoa  14220  cycsubg2  14977  cntzval  15120  cntzsnval  15123  odfval  15171  odval  15172  gexval  15212  efgsfo  15371  dprdval  15561  ablfac1a  15627  ablfac1b  15628  ablfac1eu  15631  ablfaclem1  15643  ablfaclem3  15645  lspval  16051  aspval  16387  psrass1lem  16442  psrmulval  16450  mplmonmul  16527  coe1mul2  16662  ocvval  16894  istopon  16990  clsval  17101  neival  17166  ordtbaslem  17252  ordtbas2  17255  ordtopn1  17258  ordtopn2  17259  cnpval  17300  llyeq  17533  nllyeq  17534  xkoopn  17621  kqfval  17755  tsmsfbas  18157  blvalps  18415  blval  18416  nmofval  18748  nmoval  18749  ishtpy  18997  minveclem3b  19329  minveclem3  19330  minveclem4  19333  minveclem5  19334  ovolval  19370  vitalilem2  19501  vitalilem3  19502  vitalilem4  19503  vitali  19505  itg2monolem1  19642  elcpn  19820  mdegmullem  20001  elqaalem1  20236  elqaalem2  20237  elqaalem3  20238  elqaa  20239  aannenlem1  20245  aannenlem2  20246  jensen  20827  vmaval  20896  muval  20915  sgmval  20925  fsumdvdscom  20970  musum  20976  muinv  20978  dchrisum0fval  21199  dchrisum0ff  21201  logsqvma2  21237  pntrlog2bndlem1  21271  nbgraop1  21437  vdgrval  21667  eupath2  21702  sspval  22222  ubthlem1  22372  ubthlem2  22373  ubthlem3  22374  ocval  22782  spanval  22835  chsupid  22914  eigvecval  23399  specval  23401  measvuni  24568  brfae  24599  orvcelval  24726  ballotlemi  24758  subfacp1lem6  24871  kur14  24902  cvmscbv  24945  cvmsi  24952  cvmsval  24953  snmlval  25018  snmlflim  25019  dfpred3g  25450  fvray  26075  ftc1anclem6  26285  ptfinfin  26378  finlocfin  26379  locfindis  26385  neibastop3  26391  2rexfrabdioph  26856  3rexfrabdioph  26857  4rexfrabdioph  26858  6rexfrabdioph  26859  7rexfrabdioph  26860  eldioph4i  26873  diophren  26874  pell1qrval  26909  pell14qrval  26911  pell1234qrval  26913  rpnnen3  27103  fnwe2lem1  27125  pwssplit4  27168  pwslnmlem2  27172  dsmmelbas  27182  frlmsslss  27221  mapfien2  27235  dgraaval  27326  itgoval  27343  rgspnval  27350  proot1hash  27496  stoweidlem26  27751  stoweidlem27  27752  stoweidlem31  27756  stoweidlem34  27759  stoweidlem46  27771  2wlkonot  28332  2spthonot  28333  usg2spot2nb  28454  usgreg2spot  28456  2spotmdisj  28457  usgreghash2spot  28458  bnj602  29286  islinei  30537  pmapval  30554  paddval  30595  paddcom  30610  pclvalN  30687  ldilset  30906  dilsetN  30950  diafval  31829  diaval  31830  docavalN  31921  dicfval  31973  dochfval  32148  dochval  32149  mapdval  32426  mapdsn2  32440
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-ral 2710  df-rab 2714
  Copyright terms: Public domain W3C validator