Theorem rabbidv 3105

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 3104	1 |- ( ph -> { x e. A | ps } = { x e. A | ch } )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   e. wcel 1767   {crab 2818

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-rab 2823

This theorem is referenced by:  rabeqbidv  3108  difeq2  3616  seex  4842  mptiniseg  5501  elovmpt2rab  6505  elovmpt3rab1  6520  fineqvlem  7734  mapfien2  7868  supeq1  7905  supeq2  7908  supeq3  7909  oieq1  7937  oieq2  7938  ordtypecbv  7942  ordtypelem3  7945  harval  7988  inf3lema  8041  wemapwe  8139  wemapweOLD  8140  oef1o  8141  oef1oOLD  8142  tz9.12lem3  8207  rankvalb  8215  rankvalg  8235  ranksnb  8245  rankonidlem  8246  cardval3  8333  cardidm  8340  alephsuc2  8461  coftr  8653  fin1a2lem11  8790  fin1a2lem12  8791  hsmex  8812  axdc3lem2  8831  zorn2lem1  8876  zorn2lem6  8881  zorn2lem7  8882  zorn2g  8883  wuncval  9120  tskmval  9217  peano5uzti  10950  uzval  11084  reexALT  11214  ixxval  11537  fzval  11674  hashbclem  12467  hashbc  12468  shftfn  12869  rpnnen  13821  bitsfval  13932  sadfval  13961  sadcom  13972  smufval  13986  smupp1  13989  smupval  13997  smumullem  14001  gcdval  14005  bezoutlem2  14036  bezoutlem4  14038  isprm  14078  isprm2lem  14083  odzval  14177  pcval  14227  pceulem  14228  pceu  14229  pczpre  14230  pcdiv  14235  prmreclem1  14293  prmreclem4  14296  prmreclem5  14297  ramval  14385  cshws0  14444  imasdsval  14770  mrcval  14865  eldmcoa  15250  cycsubg2  16043  cntzval  16164  cntzsnval  16167  odfval  16363  odval  16364  gexval  16404  efgsfo  16563  dprdval  16837  dprdvalOLD  16839  ablfac1a  16922  ablfac1b  16923  ablfac1eu  16926  ablfaclem1  16938  ablfaclem3  16940  lspval  17421  aspval  17776  psrass1lem  17828  psrmulval  17838  mplmonmul  17925  coe1mul2  18109  ocvval  18493  dsmmelbas  18565  frlmsslss  18599  pmatcoe1fsupp  18997  istopon  19221  clsval  19332  neival  19397  ordtbaslem  19483  ordtbas2  19486  ordtopn1  19489  ordtopn2  19490  cnpval  19531  llyeq  19765  nllyeq  19766  xkoopn  19853  kqfval  19987  tsmsfbas  20389  blvalps  20651  blval  20652  nmofval  20984  nmoval  20985  ishtpy  21235  minveclem3b  21606  minveclem3  21607  minveclem4  21610  minveclem5  21611  ovolval  21648  vitalilem2  21781  vitalilem3  21782  vitalilem4  21783  vitali  21785  itg2monolem1  21920  elcpn  22100  mdegmullem  22241  elqaalem1  22477  elqaalem2  22478  elqaalem3  22479  elqaa  22480  aannenlem1  22486  aannenlem2  22487  jensen  23074  vmaval  23143  muval  23162  sgmval  23172  fsumdvdscom  23217  musum  23223  muinv  23225  dchrisum0fval  23446  dchrisum0ff  23448  logsqvma2  23484  pntrlog2bndlem1  23518  tglngval  23694  ttgval  23882  ttgitvval  23889  ebtwntg  23989  nbgraopALT  24128  nbgraop1  24129  wwlkn  24386  clwwlkn  24471  hashecclwwlkn1  24538  usghashecclwwlk  24539  2wlkonot  24569  2spthonot  24570  vdgrval  24600  rusgraprop4  24648  rusgrasn  24649  rusgranumwwlkl1  24650  rusgranumwlklem1  24653  rusgranumwlklem3  24655  rusgranumwlks  24660  rusgranumwlkg  24662  eupath2  24684  usg2spot2nb  24770  usgreg2spot  24772  2spotmdisj  24773  usgreghash2spot  24774  numclwwlkdisj  24785  numclwwlk3lem  24813  numclwwlk5  24817  sspval  25340  ubthlem1  25490  ubthlem2  25491  ubthlem3  25492  ocval  25902  spanval  25955  chsupid  26034  eigvecval  26519  specval  26521  iunpreima  27133  ordtrest2NEW  27569  ordtconlem1  27570  measvuni  27853  brfae  27888  omsfval  27933  orvcelval  28075  ballotlemi  28107  subfacp1lem6  28297  kur14  28328  cvmscbv  28371  cvmsi  28378  cvmsval  28379  snmlval  28444  snmlflim  28445  dfpred3g  28860  fvray  29396  fin2so  29645  ftc1anclem6  29700  ptfinfin  29798  finlocfin  29799  locfindis  29805  neibastop3  29811  2rexfrabdioph  30361  3rexfrabdioph  30362  4rexfrabdioph  30363  6rexfrabdioph  30364  7rexfrabdioph  30365  eldioph4i  30378  diophren  30379  pell1qrval  30414  pell14qrval  30416  pell1234qrval  30418  rpnnen3  30606  fnwe2lem1  30628  pwssplit4  30667  pwslnmlem2  30671  mapfien2OLD  30674  dgraaval  30726  itgoval  30743  rgspnval  30750  proot1hash  30793  lcmval  30826  nzss  30850  stoweidlem26  31354  stoweidlem27  31355  stoweidlem31  31359  stoweidlem34  31362  stoweidlem46  31374  fourierdlem79  31514  fourierdlem96  31531  fourierdlem97  31532  fourierdlem98  31533  fourierdlem99  31534  fourierdlem105  31540  fourierdlem107  31542  bnj602  33070  islinei  34554  pmapval  34571  paddval  34612  paddcom  34627  pclvalN  34704  ldilset  34923  dilsetN  34967  diafval  35846  diaval  35847  docavalN  35938  dicfval  35990  dochfval  36165  dochval  36166  mapdval  36443  mapdsn2  36457