Theorem rabbidv 3068

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1370   e. wcel 1758   {crab 2802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-ral 2803  df-rab 2807

This theorem is referenced by:  rabeqbidv  3071  difeq2  3575  seex  4790  mptiniseg  5439  fineqvlem  7637  mapfien2  7768  supeq1  7805  supeq2  7808  supeq3  7809  oieq1  7836  oieq2  7837  ordtypecbv  7841  ordtypelem3  7844  harval  7887  inf3lema  7940  wemapwe  8038  wemapweOLD  8039  oef1o  8040  oef1oOLD  8041  tz9.12lem3  8106  rankvalb  8114  rankvalg  8134  ranksnb  8144  rankonidlem  8145  cardval3  8232  cardidm  8239  alephsuc2  8360  coftr  8552  fin1a2lem11  8689  fin1a2lem12  8690  hsmex  8711  axdc3lem2  8730  zorn2lem1  8775  zorn2lem6  8780  zorn2lem7  8781  zorn2g  8782  wuncval  9019  tskmval  9116  peano5uzti  10841  uzval  10973  reexALT  11095  ixxval  11418  fzval  11555  hashbclem  12322  hashbc  12323  shftfn  12679  rpnnen  13626  bitsfval  13736  sadfval  13765  sadcom  13776  smufval  13790  smupp1  13793  smupval  13801  smumullem  13805  gcdval  13809  bezoutlem2  13840  bezoutlem4  13842  isprm  13882  isprm2lem  13887  odzval  13980  pcval  14028  pceulem  14029  pceu  14030  pczpre  14031  pcdiv  14036  prmreclem1  14094  prmreclem4  14097  prmreclem5  14098  ramval  14186  cshws0  14245  imasdsval  14571  mrcval  14666  eldmcoa  15051  cycsubg2  15836  cntzval  15957  cntzsnval  15960  odfval  16156  odval  16157  gexval  16197  efgsfo  16356  dprdval  16606  dprdvalOLD  16608  ablfac1a  16691  ablfac1b  16692  ablfac1eu  16695  ablfaclem1  16707  ablfaclem3  16709  lspval  17178  aspval  17521  psrass1lem  17569  psrmulval  17579  mplmonmul  17666  coe1mul2  17845  ocvval  18216  dsmmelbas  18288  frlmsslss  18322  istopon  18661  clsval  18772  neival  18837  ordtbaslem  18923  ordtbas2  18926  ordtopn1  18929  ordtopn2  18930  cnpval  18971  llyeq  19205  nllyeq  19206  xkoopn  19293  kqfval  19427  tsmsfbas  19829  blvalps  20091  blval  20092  nmofval  20424  nmoval  20425  ishtpy  20675  minveclem3b  21046  minveclem3  21047  minveclem4  21050  minveclem5  21051  ovolval  21088  vitalilem2  21221  vitalilem3  21222  vitalilem4  21223  vitali  21225  itg2monolem1  21360  elcpn  21540  mdegmullem  21681  elqaalem1  21917  elqaalem2  21918  elqaalem3  21919  elqaa  21920  aannenlem1  21926  aannenlem2  21927  jensen  22514  vmaval  22583  muval  22602  sgmval  22612  fsumdvdscom  22657  musum  22663  muinv  22665  dchrisum0fval  22886  dchrisum0ff  22888  logsqvma2  22924  pntrlog2bndlem1  22958  tglngval  23120  ttgval  23272  ttgitvval  23279  ebtwntg  23379  nbgraop1  23487  vdgrval  23717  eupath2  23752  sspval  24272  ubthlem1  24422  ubthlem2  24423  ubthlem3  24424  ocval  24834  spanval  24887  chsupid  24966  eigvecval  25451  specval  25453  iunpreima  26065  ordtrest2NEW  26497  ordtconlem1  26498  measvuni  26772  brfae  26807  omsfval  26852  orvcelval  26994  ballotlemi  27026  subfacp1lem6  27216  kur14  27247  cvmscbv  27290  cvmsi  27297  cvmsval  27298  snmlval  27363  snmlflim  27364  dfpred3g  27779  fvray  28315  fin2so  28563  ftc1anclem6  28619  ptfinfin  28717  finlocfin  28718  locfindis  28724  neibastop3  28730  2rexfrabdioph  29281  3rexfrabdioph  29282  4rexfrabdioph  29283  6rexfrabdioph  29284  7rexfrabdioph  29285  eldioph4i  29298  diophren  29299  pell1qrval  29334  pell14qrval  29336  pell1234qrval  29338  rpnnen3  29528  fnwe2lem1  29550  pwssplit4  29589  pwslnmlem2  29593  mapfien2OLD  29596  dgraaval  29648  itgoval  29665  rgspnval  29672  proot1hash  29715  stoweidlem26  29968  stoweidlem27  29969  stoweidlem31  29973  stoweidlem34  29976  stoweidlem46  29988  elovmpt2rab  30305  elovmpt3rab1  30310  wwlkn  30463  2wlkonot  30531  2spthonot  30532  clwwlkn  30577  hashecclwwlkn1  30655  usghashecclwwlk  30656  rusgraprop4  30703  rusgrasn  30704  rusgranumwlkl1lem1  30705  rusgranumwlklem1  30714  rusgranumwlklem3  30716  rusgranumwlks  30721  rusgranumwlkg  30723  usg2spot2nb  30805  usgreg2spot  30807  2spotmdisj  30808  usgreghash2spot  30809  numclwwlkdisj  30820  numclwwlk3lem  30848  numclwwlk5  30852  pmatcoe1fsupp  31178  bnj602  32225  islinei  33707  pmapval  33724  paddval  33765  paddcom  33780  pclvalN  33857  ldilset  34076  dilsetN  34120  diafval  34999  diaval  35000  docavalN  35091  dicfval  35143  dochfval  35318  dochval  35319  mapdval  35596  mapdsn2  35610