Theorem rabbidv 2954

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1362   e. wcel 1755   {crab 2709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-ral 2710  df-rab 2714

This theorem is referenced by:  rabeqbidv  2957  difeq2  3456  seex  4670  mptiniseg  5320  fineqvlem  7515  mapfien2  7646  supeq1  7683  supeq2  7686  supeq3  7687  oieq1  7714  oieq2  7715  ordtypecbv  7719  ordtypelem3  7722  harval  7765  inf3lema  7818  wemapwe  7916  wemapweOLD  7917  oef1o  7918  oef1oOLD  7919  tz9.12lem3  7984  rankvalb  7992  rankvalg  8012  ranksnb  8022  rankonidlem  8023  cardval3  8110  cardidm  8117  alephsuc2  8238  coftr  8430  fin1a2lem11  8567  fin1a2lem12  8568  hsmex  8589  axdc3lem2  8608  zorn2lem1  8653  zorn2lem6  8658  zorn2lem7  8659  zorn2g  8660  wuncval  8897  tskmval  8994  peano5uzti  10719  uzval  10851  reexALT  10973  ixxval  11296  fzval  11426  hashbclem  12189  hashbc  12190  shftfn  12546  rpnnen  13492  bitsfval  13602  sadfval  13631  sadcom  13642  smufval  13656  smupp1  13659  smupval  13667  smumullem  13671  gcdval  13675  bezoutlem2  13706  bezoutlem4  13708  isprm  13748  isprm2lem  13753  odzval  13846  pcval  13894  pceulem  13895  pceu  13896  pczpre  13897  pcdiv  13902  prmreclem1  13960  prmreclem4  13963  prmreclem5  13964  ramval  14052  cshws0  14111  imasdsval  14436  mrcval  14531  eldmcoa  14916  cycsubg2  15698  cntzval  15819  cntzsnval  15822  odfval  16016  odval  16017  gexval  16057  efgsfo  16216  dprdval  16459  dprdvalOLD  16461  ablfac1a  16544  ablfac1b  16545  ablfac1eu  16548  ablfaclem1  16560  ablfaclem3  16562  lspval  16978  aspval  17321  psrass1lem  17381  psrmulval  17391  mplmonmul  17477  coe1mul2  17621  ocvval  17934  dsmmelbas  18006  frlmsslss  18040  istopon  18372  clsval  18483  neival  18548  ordtbaslem  18634  ordtbas2  18637  ordtopn1  18640  ordtopn2  18641  cnpval  18682  llyeq  18916  nllyeq  18917  xkoopn  19004  kqfval  19138  tsmsfbas  19540  blvalps  19802  blval  19803  nmofval  20135  nmoval  20136  ishtpy  20386  minveclem3b  20757  minveclem3  20758  minveclem4  20761  minveclem5  20762  ovolval  20799  vitalilem2  20931  vitalilem3  20932  vitalilem4  20933  vitali  20935  itg2monolem1  21070  elcpn  21250  mdegmullem  21434  elqaalem1  21670  elqaalem2  21671  elqaalem3  21672  elqaa  21673  aannenlem1  21679  aannenlem2  21680  jensen  22267  vmaval  22336  muval  22355  sgmval  22365  fsumdvdscom  22410  musum  22416  muinv  22418  dchrisum0fval  22639  dchrisum0ff  22641  logsqvma2  22677  pntrlog2bndlem1  22711  tglngval  22864  ttgval  22944  ttgitvval  22951  ebtwntg  23051  nbgraop1  23159  vdgrval  23389  eupath2  23424  sspval  23944  ubthlem1  24094  ubthlem2  24095  ubthlem3  24096  ocval  24506  spanval  24559  chsupid  24638  eigvecval  25123  specval  25125  iunpreima  25739  ordtrest2NEW  26207  ordtconlem1  26208  measvuni  26482  brfae  26518  orvcelval  26699  ballotlemi  26731  subfacp1lem6  26921  kur14  26952  cvmscbv  26995  cvmsi  27002  cvmsval  27003  snmlval  27068  snmlflim  27069  dfpred3g  27483  fvray  28019  fin2so  28260  ftc1anclem6  28316  ptfinfin  28414  finlocfin  28415  locfindis  28421  neibastop3  28427  2rexfrabdioph  28979  3rexfrabdioph  28980  4rexfrabdioph  28981  6rexfrabdioph  28982  7rexfrabdioph  28983  eldioph4i  28996  diophren  28997  pell1qrval  29032  pell14qrval  29034  pell1234qrval  29036  rpnnen3  29226  fnwe2lem1  29248  pwssplit4  29287  pwslnmlem2  29291  mapfien2OLD  29294  dgraaval  29346  itgoval  29363  rgspnval  29370  proot1hash  29413  stoweidlem26  29667  stoweidlem27  29668  stoweidlem31  29672  stoweidlem34  29675  stoweidlem46  29687  elovmpt2rab  30004  elovmpt3rab1  30009  wwlkn  30162  2wlkonot  30230  2spthonot  30231  clwwlkn  30276  hashecclwwlkn1  30354  usghashecclwwlk  30355  rusgraprop4  30402  rusgrasn  30403  rusgranumwlkl1lem1  30404  rusgranumwlklem1  30413  rusgranumwlklem3  30415  rusgranumwlks  30420  rusgranumwlkg  30422  usg2spot2nb  30504  usgreg2spot  30506  2spotmdisj  30507  usgreghash2spot  30508  numclwwlkdisj  30519  numclwwlk3lem  30547  numclwwlk5  30551  bnj602  31631  islinei  32978  pmapval  32995  paddval  33036  paddcom  33051  pclvalN  33128  ldilset  33347  dilsetN  33391  diafval  34270  diaval  34271  docavalN  34362  dicfval  34414  dochfval  34589  dochval  34590  mapdval  34867  mapdsn2  34881