Theorem abbidv 2352

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1398   {cab 2218

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225

This theorem is referenced by:  rabbidva2  2797  cdeqab  3032  sbceqbid  3049  csbeq1  3141  sbcel12g  3153  sbceqg  3154  csbeq2  3162  csbeq2d  3163  csbnestgf  3191  csbprc  3554  ifbi  3643  pweq  3672  sneq  3700  csbsng  3750  rabsn  3756  dfopg  3881  opeq1  3883  opeq2  3884  csbunig  3922  unieq  3923  inteq  3952  iineq1  4005  iineq2  4008  dfiin2g  4024  iinrabm  4054  iinxprg  4066  opabbid  4175  dcextest  4703  csbxpg  4831  csbdmg  4950  imasng  5127  csbrng  5224  iotaeq  5321  iotabi  5322  dfimafn  5725  fnsnfv  5736  fndmin  5785  fliftf  5972  oprabbid  6106  recseq  6537  freceq1  6623  freceq2  6624  frec0g  6628  freccllem  6633  frecfcllem  6635  frecsuclem  6637  frecsuc  6638  qseq1  6817  qseq2  6818  qsinxp  6845  mapvalg  6892  ixpsnval  6936  ixpeq1  6944  snexxph  7220  fival  7257  acneq  7509  prplnqu  7935  cauappcvgprlemlim  7976  caucvgprprlemell  8000  caucvgprprlemelu  8001  caucvgprprlemcbv  8002  caucvgprprlemval  8003  caucvgprprlemnkeqj  8005  caucvgprprlemml  8009  caucvgprprlemmu  8010  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemopu  8014  caucvgprprlemloc  8018  caucvgprprlemclphr  8020  caucvgprprlemexbt  8021  caucvgprprlem1  8024  caucvgprprlem2  8025  caucvgsr  8117  pitonnlem2  8162  pitonn  8163  recidpipr  8171  nntopi  8209  axcaucvglemval  8212  csbwrdg  11254  shftlem  11501  shftfibg  11505  shftdm  11507  shftfib  11508  negfi  11913  tgval  13475  ptex  13477  eqglact  13942  isghm  13960  ixpsnbasval  14614  plyval  15597  vtxdfifiun  16292