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

Theorem rabbidv 2959
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 465 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
32rabbidva 2958 1  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  A  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369    e. wcel 1756   {crab 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-ral 2715  df-rab 2719
This theorem is referenced by:  rabeqbidv  2962  difeq2  3463  seex  4678  mptiniseg  5327  fineqvlem  7519  mapfien2  7650  supeq1  7687  supeq2  7690  supeq3  7691  oieq1  7718  oieq2  7719  ordtypecbv  7723  ordtypelem3  7726  harval  7769  inf3lema  7822  wemapwe  7920  wemapweOLD  7921  oef1o  7922  oef1oOLD  7923  tz9.12lem3  7988  rankvalb  7996  rankvalg  8016  ranksnb  8026  rankonidlem  8027  cardval3  8114  cardidm  8121  alephsuc2  8242  coftr  8434  fin1a2lem11  8571  fin1a2lem12  8572  hsmex  8593  axdc3lem2  8612  zorn2lem1  8657  zorn2lem6  8662  zorn2lem7  8663  zorn2g  8664  wuncval  8901  tskmval  8998  peano5uzti  10723  uzval  10855  reexALT  10977  ixxval  11300  fzval  11431  hashbclem  12197  hashbc  12198  shftfn  12554  rpnnen  13501  bitsfval  13611  sadfval  13640  sadcom  13651  smufval  13665  smupp1  13668  smupval  13676  smumullem  13680  gcdval  13684  bezoutlem2  13715  bezoutlem4  13717  isprm  13757  isprm2lem  13762  odzval  13855  pcval  13903  pceulem  13904  pceu  13905  pczpre  13906  pcdiv  13911  prmreclem1  13969  prmreclem4  13972  prmreclem5  13973  ramval  14061  cshws0  14120  imasdsval  14445  mrcval  14540  eldmcoa  14925  cycsubg2  15709  cntzval  15830  cntzsnval  15833  odfval  16027  odval  16028  gexval  16068  efgsfo  16227  dprdval  16473  dprdvalOLD  16475  ablfac1a  16558  ablfac1b  16559  ablfac1eu  16562  ablfaclem1  16574  ablfaclem3  16576  lspval  17033  aspval  17376  psrass1lem  17424  psrmulval  17434  mplmonmul  17520  coe1mul2  17698  ocvval  18067  dsmmelbas  18139  frlmsslss  18173  istopon  18505  clsval  18616  neival  18681  ordtbaslem  18767  ordtbas2  18770  ordtopn1  18773  ordtopn2  18774  cnpval  18815  llyeq  19049  nllyeq  19050  xkoopn  19137  kqfval  19271  tsmsfbas  19673  blvalps  19935  blval  19936  nmofval  20268  nmoval  20269  ishtpy  20519  minveclem3b  20890  minveclem3  20891  minveclem4  20894  minveclem5  20895  ovolval  20932  vitalilem2  21064  vitalilem3  21065  vitalilem4  21066  vitali  21068  itg2monolem1  21203  elcpn  21383  mdegmullem  21524  elqaalem1  21760  elqaalem2  21761  elqaalem3  21762  elqaa  21763  aannenlem1  21769  aannenlem2  21770  jensen  22357  vmaval  22426  muval  22445  sgmval  22455  fsumdvdscom  22500  musum  22506  muinv  22508  dchrisum0fval  22729  dchrisum0ff  22731  logsqvma2  22767  pntrlog2bndlem1  22801  tglngval  22959  ttgval  23072  ttgitvval  23079  ebtwntg  23179  nbgraop1  23287  vdgrval  23517  eupath2  23552  sspval  24072  ubthlem1  24222  ubthlem2  24223  ubthlem3  24224  ocval  24634  spanval  24687  chsupid  24766  eigvecval  25251  specval  25253  iunpreima  25866  ordtrest2NEW  26305  ordtconlem1  26306  measvuni  26580  brfae  26616  omsfval  26661  orvcelval  26803  ballotlemi  26835  subfacp1lem6  27025  kur14  27056  cvmscbv  27099  cvmsi  27106  cvmsval  27107  snmlval  27172  snmlflim  27173  dfpred3g  27587  fvray  28123  fin2so  28369  ftc1anclem6  28425  ptfinfin  28523  finlocfin  28524  locfindis  28530  neibastop3  28536  2rexfrabdioph  29087  3rexfrabdioph  29088  4rexfrabdioph  29089  6rexfrabdioph  29090  7rexfrabdioph  29091  eldioph4i  29104  diophren  29105  pell1qrval  29140  pell14qrval  29142  pell1234qrval  29144  rpnnen3  29334  fnwe2lem1  29356  pwssplit4  29395  pwslnmlem2  29399  mapfien2OLD  29402  dgraaval  29454  itgoval  29471  rgspnval  29478  proot1hash  29521  stoweidlem26  29774  stoweidlem27  29775  stoweidlem31  29779  stoweidlem34  29782  stoweidlem46  29794  elovmpt2rab  30111  elovmpt3rab1  30116  wwlkn  30269  2wlkonot  30337  2spthonot  30338  clwwlkn  30383  hashecclwwlkn1  30461  usghashecclwwlk  30462  rusgraprop4  30509  rusgrasn  30510  rusgranumwlkl1lem1  30511  rusgranumwlklem1  30520  rusgranumwlklem3  30522  rusgranumwlks  30527  rusgranumwlkg  30529  usg2spot2nb  30611  usgreg2spot  30613  2spotmdisj  30614  usgreghash2spot  30615  numclwwlkdisj  30626  numclwwlk3lem  30654  numclwwlk5  30658  pmatcollpw2lem  30820  bnj602  31795  islinei  33224  pmapval  33241  paddval  33282  paddcom  33297  pclvalN  33374  ldilset  33593  dilsetN  33637  diafval  34516  diaval  34517  docavalN  34608  dicfval  34660  dochfval  34835  dochval  34836  mapdval  35113  mapdsn2  35127
  Copyright terms: Public domain W3C validator