Theorem abbidv 2295

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1353   {cab 2163

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170

This theorem is referenced by:  rabbidva2  2725  cdeqab  2953  sbceqbid  2970  csbeq1  3061  sbcel12g  3073  sbceqg  3074  csbeq2  3082  csbeq2d  3083  csbnestgf  3110  csbprc  3469  ifbi  3555  pweq  3579  sneq  3604  csbsng  3654  rabsn  3660  dfopg  3777  opeq1  3779  opeq2  3780  csbunig  3818  unieq  3819  inteq  3848  iineq1  3901  iineq2  3904  dfiin2g  3920  iinrabm  3950  iinxprg  3962  opabbid  4069  dcextest  4581  csbxpg  4708  csbdmg  4822  imasng  4994  csbrng  5091  iotaeq  5187  iotabi  5188  dfimafn  5565  fnsnfv  5576  fndmin  5624  fliftf  5800  oprabbid  5928  recseq  6307  freceq1  6393  freceq2  6394  frec0g  6398  freccllem  6403  frecfcllem  6405  frecsuclem  6407  frecsuc  6408  qseq1  6583  qseq2  6584  qsinxp  6611  mapvalg  6658  ixpsnval  6701  ixpeq1  6709  snexxph  6949  fival  6969  prplnqu  7619  cauappcvgprlemlim  7660  caucvgprprlemell  7684  caucvgprprlemelu  7685  caucvgprprlemcbv  7686  caucvgprprlemval  7687  caucvgprprlemnkeqj  7689  caucvgprprlemml  7693  caucvgprprlemmu  7694  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemopu  7698  caucvgprprlemloc  7702  caucvgprprlemclphr  7704  caucvgprprlemexbt  7705  caucvgprprlem1  7708  caucvgprprlem2  7709  caucvgsr  7801  pitonnlem2  7846  pitonn  7847  recidpipr  7855  nntopi  7893  axcaucvglemval  7896  shftlem  10825  shftfibg  10829  shftdm  10831  shftfib  10832  negfi  11236  tgval  12711  ptex  12713  eqglact  13084