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

Theorem rabbidv 2884
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 2883 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 1717   {crab 2646
This theorem is referenced by:  rabeqbidv  2887  difeq2  3395  seex  4479  mptiniseg  5297  fineqvlem  7252  supeq1  7378  supeq2  7381  oieq1  7407  oieq2  7408  ordtypecbv  7412  ordtypelem3  7415  harval  7456  inf3lema  7505  wemapwe  7580  oef1o  7581  tz9.12lem3  7641  rankvalb  7649  rankvalg  7669  ranksnb  7679  rankonidlem  7680  cardval3  7765  cardidm  7772  alephsuc2  7887  coftr  8079  fin1a2lem11  8216  fin1a2lem12  8217  hsmex  8238  axdc3lem2  8257  zorn2lem1  8302  zorn2lem6  8307  zorn2lem7  8308  zorn2g  8309  wuncval  8543  tskmval  8640  peano5uzti  10284  uzval  10415  reexALT  10531  ixxval  10849  fzval  10970  hashbclem  11621  hashbc  11622  shftfn  11808  rpnnen  12746  bitsfval  12855  sadfval  12884  sadcom  12895  smufval  12909  smupp1  12912  smupval  12920  smumullem  12924  gcdval  12928  bezoutlem2  12959  bezoutlem4  12961  isprm  13001  isprm2lem  13006  odzval  13097  pcval  13138  pceulem  13139  pceu  13140  pczpre  13141  pcdiv  13146  prmreclem1  13204  prmreclem4  13207  prmreclem5  13208  ramval  13296  imasdsval  13661  mrcval  13755  eldmcoa  14140  cycsubg2  14897  cntzval  15040  cntzsnval  15043  odfval  15091  odval  15092  gexval  15132  efgsfo  15291  dprdval  15481  ablfac1a  15547  ablfac1b  15548  ablfac1eu  15551  ablfaclem1  15563  ablfaclem3  15565  lspval  15971  aspval  16307  psrass1lem  16362  psrmulval  16370  mplmonmul  16447  coe1mul2  16582  ocvval  16810  istopon  16906  clsval  17017  neival  17082  ordtbaslem  17167  ordtbas2  17170  ordtopn1  17173  ordtopn2  17174  cnpval  17215  llyeq  17447  nllyeq  17448  xkoopn  17535  kqfval  17669  tsmsfbas  18071  blval  18315  nmofval  18612  nmoval  18613  ishtpy  18861  minveclem3b  19189  minveclem3  19190  minveclem4  19193  minveclem5  19194  ovolval  19230  vitalilem2  19361  vitalilem3  19362  vitalilem4  19363  vitali  19365  itg2monolem1  19502  elcpn  19680  mdegmullem  19861  elqaalem1  20096  elqaalem2  20097  elqaalem3  20098  elqaa  20099  aannenlem1  20105  aannenlem2  20106  jensen  20687  vmaval  20756  muval  20775  sgmval  20785  fsumdvdscom  20830  musum  20836  muinv  20838  dchrisum0fval  21059  dchrisum0ff  21061  logsqvma2  21097  pntrlog2bndlem1  21131  nbgraop1  21296  vdgrval  21508  eupath2  21543  sspval  22063  ubthlem1  22213  ubthlem2  22214  ubthlem3  22215  ocval  22623  spanval  22676  chsupid  22755  eigvecval  23240  specval  23242  measvuni  24355  brfae  24386  orvcelval  24498  ballotlemi  24530  subfacp1lem6  24643  kur14  24674  cvmscbv  24717  cvmsi  24724  cvmsval  24725  snmlval  24790  snmlflim  24791  fvray  25782  ptfinfin  26062  finlocfin  26063  locfindis  26069  neibastop3  26075  2rexfrabdioph  26540  3rexfrabdioph  26541  4rexfrabdioph  26542  6rexfrabdioph  26543  7rexfrabdioph  26544  eldioph4i  26557  diophren  26558  pell1qrval  26593  pell14qrval  26595  pell1234qrval  26597  rpnnen3  26787  fnwe2lem1  26809  pwssplit4  26853  pwslnmlem2  26857  dsmmelbas  26867  frlmsslss  26906  mapfien2  26920  dgraaval  27011  itgoval  27028  rgspnval  27035  proot1hash  27181  stoweidlem26  27436  stoweidlem27  27437  stoweidlem31  27441  stoweidlem34  27444  stoweidlem46  27456  bnj602  28617  islinei  29905  pmapval  29922  paddval  29963  paddcom  29978  pclvalN  30055  ldilset  30274  dilsetN  30318  diafval  31197  diaval  31198  docavalN  31289  dicfval  31341  dochfval  31516  dochval  31517  mapdval  31794  mapdsn2  31808
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
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 2367  df-cleq 2373  df-ral 2647  df-rab 2651
  Copyright terms: Public domain W3C validator