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  3496  ifbi  3581  pweq  3608  sneq  3633  csbsng  3683  rabsn  3689  dfopg  3806  opeq1  3808  opeq2  3809  csbunig  3847  unieq  3848  inteq  3877  iineq1  3930  iineq2  3933  dfiin2g  3949  iinrabm  3979  iinxprg  3991  opabbid  4098  dcextest  4617  csbxpg  4744  csbdmg  4860  imasng  5034  csbrng  5131  iotaeq  5227  iotabi  5228  dfimafn  5609  fnsnfv  5620  fndmin  5669  fliftf  5846  oprabbid  5975  recseq  6364  freceq1  6450  freceq2  6451  frec0g  6455  freccllem  6460  frecfcllem  6462  frecsuclem  6464  frecsuc  6465  qseq1  6642  qseq2  6643  qsinxp  6670  mapvalg  6717  ixpsnval  6760  ixpeq1  6768  snexxph  7016  fival  7036  prplnqu  7687  cauappcvgprlemlim  7728  caucvgprprlemell  7752  caucvgprprlemelu  7753  caucvgprprlemcbv  7754  caucvgprprlemval  7755  caucvgprprlemnkeqj  7757  caucvgprprlemml  7761  caucvgprprlemmu  7762  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemopu  7766  caucvgprprlemloc  7770  caucvgprprlemclphr  7772  caucvgprprlemexbt  7773  caucvgprprlem1  7776  caucvgprprlem2  7777  caucvgsr  7869  pitonnlem2  7914  pitonn  7915  recidpipr  7923  nntopi  7961  axcaucvglemval  7964  csbwrdg  10964  shftlem  10981  shftfibg  10985  shftdm  10987  shftfib  10988  negfi  11393  tgval  12933  ptex  12935  eqglact  13355  isghm  13373  ixpsnbasval  14022  plyval  14968