Theorem abbidv 2322

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1372   {cab 2190

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197

This theorem is referenced by:  rabbidva2  2758  cdeqab  2987  sbceqbid  3004  csbeq1  3095  sbcel12g  3107  sbceqg  3108  csbeq2  3116  csbeq2d  3117  csbnestgf  3145  csbprc  3505  ifbi  3590  pweq  3618  sneq  3643  csbsng  3693  rabsn  3699  dfopg  3816  opeq1  3818  opeq2  3819  csbunig  3857  unieq  3858  inteq  3887  iineq1  3940  iineq2  3943  dfiin2g  3959  iinrabm  3989  iinxprg  4001  opabbid  4108  dcextest  4628  csbxpg  4755  csbdmg  4871  imasng  5046  csbrng  5143  iotaeq  5239  iotabi  5240  dfimafn  5626  fnsnfv  5637  fndmin  5686  fliftf  5867  oprabbid  5997  recseq  6391  freceq1  6477  freceq2  6478  frec0g  6482  freccllem  6487  frecfcllem  6489  frecsuclem  6491  frecsuc  6492  qseq1  6669  qseq2  6670  qsinxp  6697  mapvalg  6744  ixpsnval  6787  ixpeq1  6795  snexxph  7051  fival  7071  acneq  7313  prplnqu  7732  cauappcvgprlemlim  7773  caucvgprprlemell  7797  caucvgprprlemelu  7798  caucvgprprlemcbv  7799  caucvgprprlemval  7800  caucvgprprlemnkeqj  7802  caucvgprprlemml  7806  caucvgprprlemmu  7807  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemopu  7811  caucvgprprlemloc  7815  caucvgprprlemclphr  7817  caucvgprprlemexbt  7818  caucvgprprlem1  7821  caucvgprprlem2  7822  caucvgsr  7914  pitonnlem2  7959  pitonn  7960  recidpipr  7968  nntopi  8006  axcaucvglemval  8009  csbwrdg  11021  shftlem  11098  shftfibg  11102  shftdm  11104  shftfib  11105  negfi  11510  tgval  13065  ptex  13067  eqglact  13532  isghm  13550  ixpsnbasval  14199  plyval  15175