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  3854  opeq1  3856  opeq2  3857  csbunig  3895  unieq  3896  inteq  3925  iineq1  3978  iineq2  3981  dfiin2g  3997  iinrabm  4027  iinxprg  4039  opabbid  4148  dcextest  4672  csbxpg  4799  csbdmg  4916  imasng  5092  csbrng  5189  iotaeq  5286  iotabi  5287  dfimafn  5681  fnsnfv  5692  fndmin  5741  fliftf  5922  oprabbid  6056  recseq  6450  freceq1  6536  freceq2  6537  frec0g  6541  freccllem  6546  frecfcllem  6548  frecsuclem  6550  frecsuc  6551  qseq1  6728  qseq2  6729  qsinxp  6756  mapvalg  6803  ixpsnval  6846  ixpeq1  6854  snexxph  7113  fival  7133  acneq  7380  prplnqu  7803  cauappcvgprlemlim  7844  caucvgprprlemell  7868  caucvgprprlemelu  7869  caucvgprprlemcbv  7870  caucvgprprlemval  7871  caucvgprprlemnkeqj  7873  caucvgprprlemml  7877  caucvgprprlemmu  7878  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemopu  7882  caucvgprprlemloc  7886  caucvgprprlemclphr  7888  caucvgprprlemexbt  7889  caucvgprprlem1  7892  caucvgprprlem2  7893  caucvgsr  7985  pitonnlem2  8030  pitonn  8031  recidpipr  8039  nntopi  8077  axcaucvglemval  8080  csbwrdg  11096  shftlem  11322  shftfibg  11326  shftdm  11328  shftfib  11329  negfi  11734  tgval  13290  ptex  13292  eqglact  13757  isghm  13775  ixpsnbasval  14424  plyval  15400