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

Theorem rabbidv 2892
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 2891 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 2654
This theorem is referenced by:  rabeqbidv  2895  difeq2  3403  seex  4487  mptiniseg  5305  fineqvlem  7260  supeq1  7386  supeq2  7389  oieq1  7415  oieq2  7416  ordtypecbv  7420  ordtypelem3  7423  harval  7464  inf3lema  7513  wemapwe  7588  oef1o  7589  tz9.12lem3  7649  rankvalb  7657  rankvalg  7677  ranksnb  7687  rankonidlem  7688  cardval3  7773  cardidm  7780  alephsuc2  7895  coftr  8087  fin1a2lem11  8224  fin1a2lem12  8225  hsmex  8246  axdc3lem2  8265  zorn2lem1  8310  zorn2lem6  8315  zorn2lem7  8316  zorn2g  8317  wuncval  8551  tskmval  8648  peano5uzti  10292  uzval  10423  reexALT  10539  ixxval  10857  fzval  10978  hashbclem  11629  hashbc  11630  shftfn  11816  rpnnen  12754  bitsfval  12863  sadfval  12892  sadcom  12903  smufval  12917  smupp1  12920  smupval  12928  smumullem  12932  gcdval  12936  bezoutlem2  12967  bezoutlem4  12969  isprm  13009  isprm2lem  13014  odzval  13105  pcval  13146  pceulem  13147  pceu  13148  pczpre  13149  pcdiv  13154  prmreclem1  13212  prmreclem4  13215  prmreclem5  13216  ramval  13304  imasdsval  13669  mrcval  13763  eldmcoa  14148  cycsubg2  14905  cntzval  15048  cntzsnval  15051  odfval  15099  odval  15100  gexval  15140  efgsfo  15299  dprdval  15489  ablfac1a  15555  ablfac1b  15556  ablfac1eu  15559  ablfaclem1  15571  ablfaclem3  15573  lspval  15979  aspval  16315  psrass1lem  16370  psrmulval  16378  mplmonmul  16455  coe1mul2  16590  ocvval  16818  istopon  16914  clsval  17025  neival  17090  ordtbaslem  17175  ordtbas2  17178  ordtopn1  17181  ordtopn2  17182  cnpval  17223  llyeq  17455  nllyeq  17456  xkoopn  17543  kqfval  17677  tsmsfbas  18079  blval  18323  nmofval  18620  nmoval  18621  ishtpy  18869  minveclem3b  19197  minveclem3  19198  minveclem4  19201  minveclem5  19202  ovolval  19238  vitalilem2  19369  vitalilem3  19370  vitalilem4  19371  vitali  19373  itg2monolem1  19510  elcpn  19688  mdegmullem  19869  elqaalem1  20104  elqaalem2  20105  elqaalem3  20106  elqaa  20107  aannenlem1  20113  aannenlem2  20114  jensen  20695  vmaval  20764  muval  20783  sgmval  20793  fsumdvdscom  20838  musum  20844  muinv  20846  dchrisum0fval  21067  dchrisum0ff  21069  logsqvma2  21105  pntrlog2bndlem1  21139  nbgraop1  21304  vdgrval  21516  eupath2  21551  sspval  22071  ubthlem1  22221  ubthlem2  22222  ubthlem3  22223  ocval  22631  spanval  22684  chsupid  22763  eigvecval  23248  specval  23250  measvuni  24363  brfae  24394  orvcelval  24506  ballotlemi  24538  subfacp1lem6  24651  kur14  24682  cvmscbv  24725  cvmsi  24732  cvmsval  24733  snmlval  24798  snmlflim  24799  fvray  25790  ptfinfin  26070  finlocfin  26071  locfindis  26077  neibastop3  26083  2rexfrabdioph  26548  3rexfrabdioph  26549  4rexfrabdioph  26550  6rexfrabdioph  26551  7rexfrabdioph  26552  eldioph4i  26565  diophren  26566  pell1qrval  26601  pell14qrval  26603  pell1234qrval  26605  rpnnen3  26795  fnwe2lem1  26817  pwssplit4  26861  pwslnmlem2  26865  dsmmelbas  26875  frlmsslss  26914  mapfien2  26928  dgraaval  27019  itgoval  27036  rgspnval  27043  proot1hash  27189  stoweidlem26  27444  stoweidlem27  27445  stoweidlem31  27449  stoweidlem34  27452  stoweidlem46  27464  bnj602  28625  islinei  29855  pmapval  29872  paddval  29913  paddcom  29928  pclvalN  30005  ldilset  30224  dilsetN  30268  diafval  31147  diaval  31148  docavalN  31239  dicfval  31291  dochfval  31466  dochval  31467  mapdval  31744  mapdsn2  31758
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 2369
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 2375  df-cleq 2381  df-ral 2655  df-rab 2659
  Copyright terms: Public domain W3C validator