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  3577  sneq  3602  csbsng  3652  rabsn  3658  dfopg  3774  opeq1  3776  opeq2  3777  csbunig  3815  unieq  3816  inteq  3845  iineq1  3898  iineq2  3901  dfiin2g  3917  iinrabm  3946  iinxprg  3958  opabbid  4065  dcextest  4577  csbxpg  4704  csbdmg  4817  imasng  4989  csbrng  5086  iotaeq  5182  iotabi  5183  dfimafn  5560  fnsnfv  5571  fndmin  5619  fliftf  5794  oprabbid  5922  recseq  6301  freceq1  6387  freceq2  6388  frec0g  6392  freccllem  6397  frecfcllem  6399  frecsuclem  6401  frecsuc  6402  qseq1  6577  qseq2  6578  qsinxp  6605  mapvalg  6652  ixpsnval  6695  ixpeq1  6703  snexxph  6943  fival  6963  prplnqu  7607  cauappcvgprlemlim  7648  caucvgprprlemell  7672  caucvgprprlemelu  7673  caucvgprprlemcbv  7674  caucvgprprlemval  7675  caucvgprprlemnkeqj  7677  caucvgprprlemml  7681  caucvgprprlemmu  7682  caucvgprprlemopl  7684  caucvgprprlemlol  7685  caucvgprprlemopu  7686  caucvgprprlemloc  7690  caucvgprprlemclphr  7692  caucvgprprlemexbt  7693  caucvgprprlem1  7696  caucvgprprlem2  7697  caucvgsr  7789  pitonnlem2  7834  pitonn  7835  recidpipr  7843  nntopi  7881  axcaucvglemval  7884  shftlem  10806  shftfibg  10810  shftdm  10812  shftfib  10813  negfi  11217  tgval  13209