Theorem abbidv 2323

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

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

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198

This theorem is referenced by:  rabbidva2  2759  cdeqab  2988  sbceqbid  3005  csbeq1  3096  sbcel12g  3108  sbceqg  3109  csbeq2  3117  csbeq2d  3118  csbnestgf  3146  csbprc  3506  ifbi  3591  pweq  3619  sneq  3644  csbsng  3694  rabsn  3700  dfopg  3817  opeq1  3819  opeq2  3820  csbunig  3858  unieq  3859  inteq  3888  iineq1  3941  iineq2  3944  dfiin2g  3960  iinrabm  3990  iinxprg  4002  opabbid  4109  dcextest  4629  csbxpg  4756  csbdmg  4872  imasng  5047  csbrng  5144  iotaeq  5240  iotabi  5241  dfimafn  5627  fnsnfv  5638  fndmin  5687  fliftf  5868  oprabbid  5998  recseq  6392  freceq1  6478  freceq2  6479  frec0g  6483  freccllem  6488  frecfcllem  6490  frecsuclem  6492  frecsuc  6493  qseq1  6670  qseq2  6671  qsinxp  6698  mapvalg  6745  ixpsnval  6788  ixpeq1  6796  snexxph  7052  fival  7072  acneq  7314  prplnqu  7733  cauappcvgprlemlim  7774  caucvgprprlemell  7798  caucvgprprlemelu  7799  caucvgprprlemcbv  7800  caucvgprprlemval  7801  caucvgprprlemnkeqj  7803  caucvgprprlemml  7807  caucvgprprlemmu  7808  caucvgprprlemopl  7810  caucvgprprlemlol  7811  caucvgprprlemopu  7812  caucvgprprlemloc  7816  caucvgprprlemclphr  7818  caucvgprprlemexbt  7819  caucvgprprlem1  7822  caucvgprprlem2  7823  caucvgsr  7915  pitonnlem2  7960  pitonn  7961  recidpipr  7969  nntopi  8007  axcaucvglemval  8010  csbwrdg  11023  shftlem  11127  shftfibg  11131  shftdm  11133  shftfib  11134  negfi  11539  tgval  13094  ptex  13096  eqglact  13561  isghm  13579  ixpsnbasval  14228  plyval  15204