Theorem abbidv 2255

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1331   {cab 2123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130

This theorem is referenced by:  rabbidva2  2668  cdeqab  2894  csbeq1  3001  sbcel12g  3012  sbceqg  3013  csbeq2  3021  csbeq2d  3022  csbnestgf  3047  csbprc  3403  ifbi  3487  pweq  3508  sneq  3533  csbsng  3579  rabsn  3585  dfopg  3698  opeq1  3700  opeq2  3701  csbunig  3739  unieq  3740  inteq  3769  iineq1  3822  iineq2  3825  dfiin2g  3841  iinrabm  3870  iinxprg  3882  opabbid  3988  dcextest  4490  csbxpg  4615  csbdmg  4728  imasng  4899  csbrng  4995  iotaeq  5091  iotabi  5092  dfimafn  5463  fnsnfv  5473  fndmin  5520  fliftf  5693  oprabbid  5817  recseq  6196  freceq1  6282  freceq2  6283  frec0g  6287  freccllem  6292  frecfcllem  6294  frecsuclem  6296  frecsuc  6297  qseq1  6470  qseq2  6471  qsinxp  6498  mapvalg  6545  ixpsnval  6588  ixpeq1  6596  snexxph  6831  fival  6851  prplnqu  7421  cauappcvgprlemlim  7462  caucvgprprlemell  7486  caucvgprprlemelu  7487  caucvgprprlemcbv  7488  caucvgprprlemval  7489  caucvgprprlemnkeqj  7491  caucvgprprlemml  7495  caucvgprprlemmu  7496  caucvgprprlemopl  7498  caucvgprprlemlol  7499  caucvgprprlemopu  7500  caucvgprprlemloc  7504  caucvgprprlemclphr  7506  caucvgprprlemexbt  7507  caucvgprprlem1  7510  caucvgprprlem2  7511  caucvgsr  7603  pitonnlem2  7648  pitonn  7649  recidpipr  7657  nntopi  7695  axcaucvglemval  7698  shftlem  10581  shftfibg  10585  shftdm  10587  shftfib  10588  negfi  10992  tgval  12207