Theorem abbidv 2325

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1373   {cab 2193

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200

This theorem is referenced by:  rabbidva2  2763  cdeqab  2995  sbceqbid  3012  csbeq1  3104  sbcel12g  3116  sbceqg  3117  csbeq2  3125  csbeq2d  3126  csbnestgf  3154  csbprc  3514  ifbi  3600  pweq  3629  sneq  3654  csbsng  3704  rabsn  3710  dfopg  3831  opeq1  3833  opeq2  3834  csbunig  3872  unieq  3873  inteq  3902  iineq1  3955  iineq2  3958  dfiin2g  3974  iinrabm  4004  iinxprg  4016  opabbid  4125  dcextest  4647  csbxpg  4774  csbdmg  4891  imasng  5066  csbrng  5163  iotaeq  5259  iotabi  5260  dfimafn  5650  fnsnfv  5661  fndmin  5710  fliftf  5891  oprabbid  6021  recseq  6415  freceq1  6501  freceq2  6502  frec0g  6506  freccllem  6511  frecfcllem  6513  frecsuclem  6515  frecsuc  6516  qseq1  6693  qseq2  6694  qsinxp  6721  mapvalg  6768  ixpsnval  6811  ixpeq1  6819  snexxph  7078  fival  7098  acneq  7345  prplnqu  7768  cauappcvgprlemlim  7809  caucvgprprlemell  7833  caucvgprprlemelu  7834  caucvgprprlemcbv  7835  caucvgprprlemval  7836  caucvgprprlemnkeqj  7838  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemopl  7845  caucvgprprlemlol  7846  caucvgprprlemopu  7847  caucvgprprlemloc  7851  caucvgprprlemclphr  7853  caucvgprprlemexbt  7854  caucvgprprlem1  7857  caucvgprprlem2  7858  caucvgsr  7950  pitonnlem2  7995  pitonn  7996  recidpipr  8004  nntopi  8042  axcaucvglemval  8045  csbwrdg  11060  shftlem  11242  shftfibg  11246  shftdm  11248  shftfib  11249  negfi  11654  tgval  13209  ptex  13211  eqglact  13676  isghm  13694  ixpsnbasval  14343  plyval  15319