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  2786  cdeqab  3018  sbceqbid  3035  csbeq1  3127  sbcel12g  3139  sbceqg  3140  csbeq2  3148  csbeq2d  3149  csbnestgf  3177  csbprc  3537  ifbi  3623  pweq  3652  sneq  3677  csbsng  3727  rabsn  3733  dfopg  3855  opeq1  3857  opeq2  3858  csbunig  3896  unieq  3897  inteq  3926  iineq1  3979  iineq2  3982  dfiin2g  3998  iinrabm  4028  iinxprg  4040  opabbid  4149  dcextest  4673  csbxpg  4800  csbdmg  4917  imasng  5093  csbrng  5190  iotaeq  5287  iotabi  5288  dfimafn  5684  fnsnfv  5695  fndmin  5744  fliftf  5929  oprabbid  6063  recseq  6458  freceq1  6544  freceq2  6545  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecsuc  6559  qseq1  6738  qseq2  6739  qsinxp  6766  mapvalg  6813  ixpsnval  6856  ixpeq1  6864  snexxph  7128  fival  7148  acneq  7395  prplnqu  7818  cauappcvgprlemlim  7859  caucvgprprlemell  7883  caucvgprprlemelu  7884  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemnkeqj  7888  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemloc  7901  caucvgprprlemclphr  7903  caucvgprprlemexbt  7904  caucvgprprlem1  7907  caucvgprprlem2  7908  caucvgsr  8000  pitonnlem2  8045  pitonn  8046  recidpipr  8054  nntopi  8092  axcaucvglemval  8095  csbwrdg  11114  shftlem  11342  shftfibg  11346  shftdm  11348  shftfib  11349  negfi  11754  tgval  13310  ptex  13312  eqglact  13777  isghm  13795  ixpsnbasval  14445  plyval  15421  vtxdfifiun  16056