Theorem abbidv 2349

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 1576	. 2 |- F/ x ph
2		abbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	abbid 2348	1 |- ( ph -> { x | ps } = { x | ch } )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1397   {cab 2217

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224

This theorem is referenced by:  rabbidva2  2786  cdeqab  3021  sbceqbid  3038  csbeq1  3130  sbcel12g  3142  sbceqg  3143  csbeq2  3151  csbeq2d  3152  csbnestgf  3180  csbprc  3540  ifbi  3626  pweq  3655  sneq  3680  csbsng  3730  rabsn  3736  dfopg  3860  opeq1  3862  opeq2  3863  csbunig  3901  unieq  3902  inteq  3931  iineq1  3984  iineq2  3987  dfiin2g  4003  iinrabm  4033  iinxprg  4045  opabbid  4154  dcextest  4679  csbxpg  4807  csbdmg  4925  imasng  5101  csbrng  5198  iotaeq  5295  iotabi  5296  dfimafn  5694  fnsnfv  5705  fndmin  5754  fliftf  5939  oprabbid  6073  recseq  6471  freceq1  6557  freceq2  6558  frec0g  6562  freccllem  6567  frecfcllem  6569  frecsuclem  6571  frecsuc  6572  qseq1  6751  qseq2  6752  qsinxp  6779  mapvalg  6826  ixpsnval  6869  ixpeq1  6877  snexxph  7148  fival  7168  acneq  7416  prplnqu  7839  cauappcvgprlemlim  7880  caucvgprprlemell  7904  caucvgprprlemelu  7905  caucvgprprlemcbv  7906  caucvgprprlemval  7907  caucvgprprlemnkeqj  7909  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemopu  7918  caucvgprprlemloc  7922  caucvgprprlemclphr  7924  caucvgprprlemexbt  7925  caucvgprprlem1  7928  caucvgprprlem2  7929  caucvgsr  8021  pitonnlem2  8066  pitonn  8067  recidpipr  8075  nntopi  8113  axcaucvglemval  8116  csbwrdg  11142  shftlem  11376  shftfibg  11380  shftdm  11382  shftfib  11383  negfi  11788  tgval  13344  ptex  13346  eqglact  13811  isghm  13829  ixpsnbasval  14479  plyval  15455  vtxdfifiun  16147