Theorem rabbidv 3036

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 467	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	rabbidva 3035	1 |- ( ph -> { x e. A | ps } = { x e. A | ch } )

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1444   e. wcel 1887   {crab 2741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-ral 2742  df-rab 2746

This theorem is referenced by:  rabeqbidv  3040  difeq2  3545  seex  4797  mptiniseg  5329  dfpred3g  5391  elovmpt2rab  6515  elovmpt3rab1  6527  fineqvlem  7786  mapfien2  7922  supeq1  7959  supeq2  7962  supeq3  7963  oieq1  8027  oieq2  8028  ordtypecbv  8032  ordtypelem3  8035  harval  8077  inf3lema  8129  wemapwe  8202  oef1o  8203  tz9.12lem3  8260  rankvalb  8268  rankvalg  8288  ranksnb  8298  rankonidlem  8299  cardval3  8386  cardidm  8393  alephsuc2  8511  coftr  8703  fin1a2lem11  8840  fin1a2lem12  8841  hsmex  8862  axdc3lem2  8881  zorn2lem1  8926  zorn2lem6  8931  zorn2lem7  8932  zorn2g  8933  wuncval  9167  tskmval  9264  peano5uzti  11025  uzval  11161  reexALT  11296  ixxval  11643  fzval  11786  hashbclem  12615  hashbc  12616  shftfn  13136  rpnnen  14279  bitsfval  14396  sadfval  14426  sadcom  14437  smufval  14451  smupp1  14454  smupval  14462  smumullem  14466  gcdval  14470  bezoutlem2OLD  14504  bezoutlem4OLD  14506  bezoutlem2  14507  bezoutlem4  14509  lcmval  14555  lcmvalOLD  14556  lcmslefacOLD  14586  lcmfval  14591  lcmf0val  14592  lcmfvalOLD  14595  lcmfpr  14600  isprm  14624  isprm2lem  14631  odzval  14736  odzvalOLD  14742  pcval  14794  pceulem  14795  pceu  14796  pczpre  14797  pcdiv  14802  prmreclem1  14860  prmreclem4  14863  prmreclem5  14864  ramval  14960  ramvalOLD  14961  prmgaplcmlem1OLD  15012  prmordvdslcmsOLDOLD  15021  prmorlelcmsOLDOLD  15022  cshws0  15072  imasdsval  15416  imasdsvalOLD  15428  mrcval  15516  eldmcoa  15960  cycsubg2  16854  cntzval  16975  cntzsnval  16978  odfval  17179  odval  17180  odfvalOLD  17182  odvalOLD  17183  gexval  17227  gexvalOLD  17229  efgsfo  17389  dprdval  17635  ablfac1a  17702  ablfac1b  17703  ablfac1eu  17706  ablfaclem1  17718  ablfaclem3  17720  lspval  18198  aspval  18552  psrass1lem  18601  psrmulval  18610  mplmonmul  18688  coe1mul2  18862  ocvval  19230  dsmmelbas  19302  frlmsslss  19332  pmatcoe1fsupp  19725  istopon  19940  clsval  20052  neival  20118  ordtbaslem  20204  ordtbas2  20207  ordtopn1  20210  ordtopn2  20211  cnpval  20252  llyeq  20485  nllyeq  20486  ptfinfin  20534  finlocfin  20535  dissnlocfin  20544  locfindis  20545  xkoopn  20604  kqfval  20738  tsmsfbas  21142  blvalps  21400  blval  21401  nmofval  21719  nmoval  21720  nmofvalOLD  21738  nmovalOLD  21739  ishtpy  22003  minveclem3b  22370  minveclem3  22371  minveclem4  22374  minveclem5  22375  minveclem3bOLD  22382  minveclem3OLD  22383  minveclem4OLD  22386  minveclem5OLD  22387  ovolval  22426  ovolvalOLD  22427  vitalilem2  22567  vitalilem3  22568  vitalilem4  22569  vitali  22571  itg2monolem1  22708  elcpn  22888  mdegmullem  23027  elqaalem1  23272  elqaalem2  23273  elqaalem3  23274  elqaalem1OLD  23275  elqaalem2OLD  23276  elqaalem3OLD  23277  elqaa  23278  aannenlem1  23284  aannenlem2  23285  jensen  23914  vmaval  24040  muval  24059  sgmval  24069  fsumdvdscom  24114  musum  24120  muinv  24122  dchrisum0fval  24343  dchrisum0ff  24345  logsqvma2  24381  pntrlog2bndlem1  24415  tglngval  24596  ttgval  24905  ttgitvval  24912  ebtwntg  25012  nbgraopALT  25152  nbgraop1  25153  wwlkn  25410  clwwlkn  25495  hashecclwwlkn1  25562  usghashecclwwlk  25563  2wlkonot  25593  2spthonot  25594  2pthwlkonot  25613  vdgrval  25624  rusgraprop4  25672  rusgrasn  25673  rusgranumwwlkl1  25674  rusgranumwlklem1  25677  rusgranumwlklem3  25679  rusgranumwlks  25684  rusgranumwlkg  25686  eupath2  25708  usg2spot2nb  25793  usgreg2spot  25795  2spotmdisj  25796  usgreghash2spot  25797  numclwwlkdisj  25808  numclwwlk3lem  25836  numclwwlk5  25840  sspval  26362  ubthlem1  26512  ubthlem2  26513  ubthlem3  26514  ocval  26933  spanval  26986  chsupid  27065  eigvecval  27549  specval  27551  iunpreima  28180  aciunf1  28265  crefeq  28672  ordtcnvNEW  28726  ordtrest2NEW  28729  ordtconlem1  28730  measvuni  29036  brfae  29071  omsfval  29118  omsfvalOLD  29122  orvcelval  29301  ballotlemi  29333  ballotlemiOLD  29371  bnj602  29726  subfacp1lem6  29908  kur14  29939  cvmscbv  29981  cvmsi  29988  cvmsval  29989  snmlval  30054  snmlflim  30055  fvray  30908  fwddifnval  30930  neibastop3  31018  icoreval  31756  fin2so  31932  poimirlem26  31966  poimirlem27  31967  poimirlem28  31968  poimirlem32  31972  ftc1anclem6  32022  islinei  33305  pmapval  33322  paddval  33363  paddcom  33378  pclvalN  33455  ldilset  33674  dilsetN  33719  diafval  34599  diaval  34600  docavalN  34691  dicfval  34743  dochfval  34918  dochval  34919  mapdval  35196  mapdsn2  35210  2rexfrabdioph  35639  3rexfrabdioph  35640  4rexfrabdioph  35641  6rexfrabdioph  35642  7rexfrabdioph  35643  eldioph4i  35655  diophren  35656  pell1qrval  35692  pell14qrval  35694  pell1234qrval  35696  rpnnen3  35887  fnwe2lem1  35908  pwssplit4  35947  pwslnmlem2  35951  dgraaval  36005  dgraavalOLD  36006  itgoval  36027  rgspnval  36034  proot1hash  36077  nzss  36666  dvnprodlem1  37821  dvnprodlem2  37822  dvnprodlem3  37823  dvnprod  37824  stoweidlem26  37886  stoweidlem27  37887  stoweidlem31  37892  stoweidlem34  37895  stoweidlem46  37907  fourierdlem79  38049  fourierdlem96  38066  fourierdlem97  38067  fourierdlem98  38068  fourierdlem99  38069  fourierdlem105  38075  fourierdlem107  38077  fourierdlem108  38078  fourierdlem110  38080  etransclem11  38110  salgenval  38182  ovnval  38362  ovnval2  38367  ovnval2b  38374  ovncvrrp  38386  ovnsubaddlem1  38392  ovnsubadd  38394  ovncvr2  38433  hspmbl  38451  dfnbgr2  39407  dfnbgr3  39408  uvtxusgr  39475  vtxdgval  39529  rnghmval  39944  bigoval  40413