Theorem rabbidv 3072

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

Step	Hyp	Ref	Expression
1		rabbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	adantr 466	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	rabbidva 3071	1 |- ( ph -> { x e. A | ps } = { x e. A | ch } )

Syntax hints:   -> wi 4   <-> wb 187   = wceq 1437   e. wcel 1868   {crab 2779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-ral 2780  df-rab 2784

This theorem is referenced by:  rabeqbidv  3076  difeq2  3577  seex  4813  mptiniseg  5345  dfpred3g  5407  elovmpt2rab  6526  elovmpt3rab1  6538  fineqvlem  7789  mapfien2  7925  supeq1  7962  supeq2  7965  supeq3  7966  oieq1  8030  oieq2  8031  ordtypecbv  8035  ordtypelem3  8038  harval  8080  inf3lema  8132  wemapwe  8204  oef1o  8205  tz9.12lem3  8262  rankvalb  8270  rankvalg  8290  ranksnb  8300  rankonidlem  8301  cardval3  8388  cardidm  8395  alephsuc2  8512  coftr  8704  fin1a2lem11  8841  fin1a2lem12  8842  hsmex  8863  axdc3lem2  8882  zorn2lem1  8927  zorn2lem6  8932  zorn2lem7  8933  zorn2g  8934  wuncval  9168  tskmval  9265  peano5uzti  11026  uzval  11162  reexALT  11297  ixxval  11644  fzval  11787  hashbclem  12613  hashbc  12614  shftfn  13125  rpnnen  14267  bitsfval  14384  sadfval  14414  sadcom  14425  smufval  14439  smupp1  14442  smupval  14450  smumullem  14454  gcdval  14458  bezoutlem2OLD  14492  bezoutlem4OLD  14494  bezoutlem2  14495  bezoutlem4  14497  lcmval  14543  lcmvalOLD  14544  lcmslefacOLD  14574  lcmfval  14579  lcmf0val  14580  lcmfvalOLD  14583  lcmfpr  14588  isprm  14612  isprm2lem  14619  odzval  14724  odzvalOLD  14730  pcval  14782  pceulem  14783  pceu  14784  pczpre  14785  pcdiv  14790  prmreclem1  14848  prmreclem4  14851  prmreclem5  14852  ramval  14948  ramvalOLD  14949  prmgaplcmlem1OLD  15000  prmordvdslcmsOLDOLD  15009  prmorlelcmsOLDOLD  15010  cshws0  15060  imasdsval  15404  imasdsvalOLD  15416  mrcval  15504  eldmcoa  15948  cycsubg2  16842  cntzval  16963  cntzsnval  16966  odfval  17167  odval  17168  odfvalOLD  17170  odvalOLD  17171  gexval  17215  gexvalOLD  17217  efgsfo  17377  dprdval  17623  ablfac1a  17690  ablfac1b  17691  ablfac1eu  17694  ablfaclem1  17706  ablfaclem3  17708  lspval  18186  aspval  18540  psrass1lem  18589  psrmulval  18598  mplmonmul  18676  coe1mul2  18850  ocvval  19217  dsmmelbas  19289  frlmsslss  19319  pmatcoe1fsupp  19712  istopon  19927  clsval  20039  neival  20105  ordtbaslem  20191  ordtbas2  20194  ordtopn1  20197  ordtopn2  20198  cnpval  20239  llyeq  20472  nllyeq  20473  ptfinfin  20521  finlocfin  20522  dissnlocfin  20531  locfindis  20532  xkoopn  20591  kqfval  20725  tsmsfbas  21129  blvalps  21387  blval  21388  nmofval  21706  nmoval  21707  nmofvalOLD  21725  nmovalOLD  21726  ishtpy  21990  minveclem3b  22357  minveclem3  22358  minveclem4  22361  minveclem5  22362  minveclem3bOLD  22369  minveclem3OLD  22370  minveclem4OLD  22373  minveclem5OLD  22374  ovolval  22413  ovolvalOLD  22414  vitalilem2  22554  vitalilem3  22555  vitalilem4  22556  vitali  22558  itg2monolem1  22695  elcpn  22875  mdegmullem  23014  elqaalem1  23259  elqaalem2  23260  elqaalem3  23261  elqaalem1OLD  23262  elqaalem2OLD  23263  elqaalem3OLD  23264  elqaa  23265  aannenlem1  23271  aannenlem2  23272  jensen  23901  vmaval  24027  muval  24046  sgmval  24056  fsumdvdscom  24101  musum  24107  muinv  24109  dchrisum0fval  24330  dchrisum0ff  24332  logsqvma2  24368  pntrlog2bndlem1  24402  tglngval  24583  ttgval  24892  ttgitvval  24899  ebtwntg  24999  nbgraopALT  25138  nbgraop1  25139  wwlkn  25396  clwwlkn  25481  hashecclwwlkn1  25548  usghashecclwwlk  25549  2wlkonot  25579  2spthonot  25580  2pthwlkonot  25599  vdgrval  25610  rusgraprop4  25658  rusgrasn  25659  rusgranumwwlkl1  25660  rusgranumwlklem1  25663  rusgranumwlklem3  25665  rusgranumwlks  25670  rusgranumwlkg  25672  eupath2  25694  usg2spot2nb  25779  usgreg2spot  25781  2spotmdisj  25782  usgreghash2spot  25783  numclwwlkdisj  25794  numclwwlk3lem  25822  numclwwlk5  25826  sspval  26348  ubthlem1  26498  ubthlem2  26499  ubthlem3  26500  ocval  26919  spanval  26972  chsupid  27051  eigvecval  27535  specval  27537  iunpreima  28170  aciunf1  28255  crefeq  28668  ordtcnvNEW  28722  ordtrest2NEW  28725  ordtconlem1  28726  measvuni  29032  brfae  29067  omsfval  29114  omsfvalOLD  29118  orvcelval  29297  ballotlemi  29329  ballotlemiOLD  29367  bnj602  29722  subfacp1lem6  29904  kur14  29935  cvmscbv  29977  cvmsi  29984  cvmsval  29985  snmlval  30050  snmlflim  30051  fvray  30901  fwddifnval  30923  neibastop3  31011  icoreval  31697  fin2so  31846  poimirlem26  31880  poimirlem27  31881  poimirlem28  31882  poimirlem32  31886  ftc1anclem6  31936  islinei  33224  pmapval  33241  paddval  33282  paddcom  33297  pclvalN  33374  ldilset  33593  dilsetN  33638  diafval  34518  diaval  34519  docavalN  34610  dicfval  34662  dochfval  34837  dochval  34838  mapdval  35115  mapdsn2  35129  2rexfrabdioph  35558  3rexfrabdioph  35559  4rexfrabdioph  35560  6rexfrabdioph  35561  7rexfrabdioph  35562  eldioph4i  35574  diophren  35575  pell1qrval  35612  pell14qrval  35614  pell1234qrval  35616  rpnnen3  35807  fnwe2lem1  35828  pwssplit4  35867  pwslnmlem2  35871  dgraaval  35925  dgraavalOLD  35926  itgoval  35947  rgspnval  35954  proot1hash  35997  nzss  36524  dvnprodlem1  37641  dvnprodlem2  37642  dvnprodlem3  37643  dvnprod  37644  stoweidlem26  37706  stoweidlem27  37707  stoweidlem31  37712  stoweidlem34  37715  stoweidlem46  37727  fourierdlem79  37869  fourierdlem96  37886  fourierdlem97  37887  fourierdlem98  37888  fourierdlem99  37889  fourierdlem105  37895  fourierdlem107  37897  fourierdlem108  37898  fourierdlem110  37900  etransclem11  37930  salgenval  37983  ovnval  38137  ovnval2  38142  ovnval2b  38149  ovncvrrp  38161  ovnsubaddlem1  38167  ovnsubadd  38169  rnghmval  39163  bigoval  39634