Theorem abbidv 2295

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   {cab 2163

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170

This theorem is referenced by:  rabbidva2  2724  cdeqab  2952  sbceqbid  2969  csbeq1  3060  sbcel12g  3072  sbceqg  3073  csbeq2  3081  csbeq2d  3082  csbnestgf  3109  csbprc  3468  ifbi  3554  pweq  3578  sneq  3603  csbsng  3653  rabsn  3659  dfopg  3775  opeq1  3777  opeq2  3778  csbunig  3816  unieq  3817  inteq  3846  iineq1  3899  iineq2  3902  dfiin2g  3918  iinrabm  3947  iinxprg  3959  opabbid  4066  dcextest  4578  csbxpg  4705  csbdmg  4818  imasng  4990  csbrng  5087  iotaeq  5183  iotabi  5184  dfimafn  5561  fnsnfv  5572  fndmin  5620  fliftf  5795  oprabbid  5923  recseq  6302  freceq1  6388  freceq2  6389  frec0g  6393  freccllem  6398  frecfcllem  6400  frecsuclem  6402  frecsuc  6403  qseq1  6578  qseq2  6579  qsinxp  6606  mapvalg  6653  ixpsnval  6696  ixpeq1  6704  snexxph  6944  fival  6964  prplnqu  7614  cauappcvgprlemlim  7655  caucvgprprlemell  7679  caucvgprprlemelu  7680  caucvgprprlemcbv  7681  caucvgprprlemval  7682  caucvgprprlemnkeqj  7684  caucvgprprlemml  7688  caucvgprprlemmu  7689  caucvgprprlemopl  7691  caucvgprprlemlol  7692  caucvgprprlemopu  7693  caucvgprprlemloc  7697  caucvgprprlemclphr  7699  caucvgprprlemexbt  7700  caucvgprprlem1  7703  caucvgprprlem2  7704  caucvgsr  7796  pitonnlem2  7841  pitonn  7842  recidpipr  7850  nntopi  7888  axcaucvglemval  7891  shftlem  10816  shftfibg  10820  shftdm  10822  shftfib  10823  negfi  11227  tgval  13331