Theorem rabbidv 2908

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

Syntax hints:   -> wi 4   <-> wb 177   = wceq 1649   e. wcel 1721   {crab 2670

This theorem is referenced by:  rabeqbidv  2911  difeq2  3419  seex  4505  mptiniseg  5323  fineqvlem  7282  supeq1  7408  supeq2  7411  oieq1  7437  oieq2  7438  ordtypecbv  7442  ordtypelem3  7445  harval  7486  inf3lema  7535  wemapwe  7610  oef1o  7611  tz9.12lem3  7671  rankvalb  7679  rankvalg  7699  ranksnb  7709  rankonidlem  7710  cardval3  7795  cardidm  7802  alephsuc2  7917  coftr  8109  fin1a2lem11  8246  fin1a2lem12  8247  hsmex  8268  axdc3lem2  8287  zorn2lem1  8332  zorn2lem6  8337  zorn2lem7  8338  zorn2g  8339  wuncval  8573  tskmval  8670  peano5uzti  10315  uzval  10446  reexALT  10562  ixxval  10880  fzval  11001  hashbclem  11656  hashbc  11657  shftfn  11843  rpnnen  12781  bitsfval  12890  sadfval  12919  sadcom  12930  smufval  12944  smupp1  12947  smupval  12955  smumullem  12959  gcdval  12963  bezoutlem2  12994  bezoutlem4  12996  isprm  13036  isprm2lem  13041  odzval  13132  pcval  13173  pceulem  13174  pceu  13175  pczpre  13176  pcdiv  13181  prmreclem1  13239  prmreclem4  13242  prmreclem5  13243  ramval  13331  imasdsval  13696  mrcval  13790  eldmcoa  14175  cycsubg2  14932  cntzval  15075  cntzsnval  15078  odfval  15126  odval  15127  gexval  15167  efgsfo  15326  dprdval  15516  ablfac1a  15582  ablfac1b  15583  ablfac1eu  15586  ablfaclem1  15598  ablfaclem3  15600  lspval  16006  aspval  16342  psrass1lem  16397  psrmulval  16405  mplmonmul  16482  coe1mul2  16617  ocvval  16849  istopon  16945  clsval  17056  neival  17121  ordtbaslem  17206  ordtbas2  17209  ordtopn1  17212  ordtopn2  17213  cnpval  17254  llyeq  17486  nllyeq  17487  xkoopn  17574  kqfval  17708  tsmsfbas  18110  blvalps  18368  blval  18369  nmofval  18701  nmoval  18702  ishtpy  18950  minveclem3b  19282  minveclem3  19283  minveclem4  19286  minveclem5  19287  ovolval  19323  vitalilem2  19454  vitalilem3  19455  vitalilem4  19456  vitali  19458  itg2monolem1  19595  elcpn  19773  mdegmullem  19954  elqaalem1  20189  elqaalem2  20190  elqaalem3  20191  elqaa  20192  aannenlem1  20198  aannenlem2  20199  jensen  20780  vmaval  20849  muval  20868  sgmval  20878  fsumdvdscom  20923  musum  20929  muinv  20931  dchrisum0fval  21152  dchrisum0ff  21154  logsqvma2  21190  pntrlog2bndlem1  21224  nbgraop1  21390  vdgrval  21620  eupath2  21655  sspval  22175  ubthlem1  22325  ubthlem2  22326  ubthlem3  22327  ocval  22735  spanval  22788  chsupid  22867  eigvecval  23352  specval  23354  measvuni  24521  brfae  24552  orvcelval  24679  ballotlemi  24711  subfacp1lem6  24824  kur14  24855  cvmscbv  24898  cvmsi  24905  cvmsval  24906  snmlval  24971  snmlflim  24972  fvray  25979  ptfinfin  26268  finlocfin  26269  locfindis  26275  neibastop3  26281  2rexfrabdioph  26746  3rexfrabdioph  26747  4rexfrabdioph  26748  6rexfrabdioph  26749  7rexfrabdioph  26750  eldioph4i  26763  diophren  26764  pell1qrval  26799  pell14qrval  26801  pell1234qrval  26803  rpnnen3  26993  fnwe2lem1  27015  pwssplit4  27059  pwslnmlem2  27063  dsmmelbas  27073  frlmsslss  27112  mapfien2  27126  dgraaval  27217  itgoval  27234  rgspnval  27241  proot1hash  27387  stoweidlem26  27642  stoweidlem27  27643  stoweidlem31  27647  stoweidlem34  27650  stoweidlem46  27662  2wlkonot  28062  2spthonot  28063  usg2spot2nb  28168  usgreg2spot  28170  2spotmdisj  28171  usgreghash2spot  28172  bnj602  28992  islinei  30222  pmapval  30239  paddval  30280  paddcom  30295  pclvalN  30372  ldilset  30591  dilsetN  30635  diafval  31514  diaval  31515  docavalN  31606  dicfval  31658  dochfval  31833  dochval  31834  mapdval  32111  mapdsn2  32125

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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

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 2391  df-cleq 2397  df-ral 2671  df-rab 2675