Theorem abbidv 2314

Description: Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.)

Hypothesis

Ref	Expression
abbidv.1	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
abbidv	|- ( ph -> { x | ps } = { x | ch } )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem abbidv

Step	Hyp	Ref	Expression
1		nfv 1542	. 2 |- F/ x ph
2		abbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	abbid 2313	1 |- ( ph -> { x | ps } = { x | ch } )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1364   {cab 2182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189

This theorem is referenced by:  rabbidva2  2750  cdeqab  2979  sbceqbid  2996  csbeq1  3087  sbcel12g  3099  sbceqg  3100  csbeq2  3108  csbeq2d  3109  csbnestgf  3137  csbprc  3497  ifbi  3582  pweq  3609  sneq  3634  csbsng  3684  rabsn  3690  dfopg  3807  opeq1  3809  opeq2  3810  csbunig  3848  unieq  3849  inteq  3878  iineq1  3931  iineq2  3934  dfiin2g  3950  iinrabm  3980  iinxprg  3992  opabbid  4099  dcextest  4618  csbxpg  4745  csbdmg  4861  imasng  5035  csbrng  5132  iotaeq  5228  iotabi  5229  dfimafn  5612  fnsnfv  5623  fndmin  5672  fliftf  5849  oprabbid  5979  recseq  6373  freceq1  6459  freceq2  6460  frec0g  6464  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  qseq1  6651  qseq2  6652  qsinxp  6679  mapvalg  6726  ixpsnval  6769  ixpeq1  6777  snexxph  7025  fival  7045  acneq  7285  prplnqu  7704  cauappcvgprlemlim  7745  caucvgprprlemell  7769  caucvgprprlemelu  7770  caucvgprprlemcbv  7771  caucvgprprlemval  7772  caucvgprprlemnkeqj  7774  caucvgprprlemml  7778  caucvgprprlemmu  7779  caucvgprprlemopl  7781  caucvgprprlemlol  7782  caucvgprprlemopu  7783  caucvgprprlemloc  7787  caucvgprprlemclphr  7789  caucvgprprlemexbt  7790  caucvgprprlem1  7793  caucvgprprlem2  7794  caucvgsr  7886  pitonnlem2  7931  pitonn  7932  recidpipr  7940  nntopi  7978  axcaucvglemval  7981  csbwrdg  10981  shftlem  10998  shftfibg  11002  shftdm  11004  shftfib  11005  negfi  11410  tgval  12964  ptex  12966  eqglact  13431  isghm  13449  ixpsnbasval  14098  plyval  15052