Theorem abbidv 2347

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1395   {cab 2215

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222

This theorem is referenced by:  rabbidva2  2784  cdeqab  3019  sbceqbid  3036  csbeq1  3128  sbcel12g  3140  sbceqg  3141  csbeq2  3149  csbeq2d  3150  csbnestgf  3178  csbprc  3538  ifbi  3624  pweq  3653  sneq  3678  csbsng  3728  rabsn  3734  dfopg  3858  opeq1  3860  opeq2  3861  csbunig  3899  unieq  3900  inteq  3929  iineq1  3982  iineq2  3985  dfiin2g  4001  iinrabm  4031  iinxprg  4043  opabbid  4152  dcextest  4677  csbxpg  4805  csbdmg  4923  imasng  5099  csbrng  5196  iotaeq  5293  iotabi  5294  dfimafn  5690  fnsnfv  5701  fndmin  5750  fliftf  5935  oprabbid  6069  recseq  6467  freceq1  6553  freceq2  6554  frec0g  6558  freccllem  6563  frecfcllem  6565  frecsuclem  6567  frecsuc  6568  qseq1  6747  qseq2  6748  qsinxp  6775  mapvalg  6822  ixpsnval  6865  ixpeq1  6873  snexxph  7140  fival  7160  acneq  7407  prplnqu  7830  cauappcvgprlemlim  7871  caucvgprprlemell  7895  caucvgprprlemelu  7896  caucvgprprlemcbv  7897  caucvgprprlemval  7898  caucvgprprlemnkeqj  7900  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemopu  7909  caucvgprprlemloc  7913  caucvgprprlemclphr  7915  caucvgprprlemexbt  7916  caucvgprprlem1  7919  caucvgprprlem2  7920  caucvgsr  8012  pitonnlem2  8057  pitonn  8058  recidpipr  8066  nntopi  8104  axcaucvglemval  8107  csbwrdg  11133  shftlem  11367  shftfibg  11371  shftdm  11373  shftfib  11374  negfi  11779  tgval  13335  ptex  13337  eqglact  13802  isghm  13820  ixpsnbasval  14470  plyval  15446  vtxdfifiun  16103