Theorem abbidv 2288

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1348   {cab 2156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163

This theorem is referenced by:  rabbidva2  2717  cdeqab  2945  csbeq1  3052  sbcel12g  3064  sbceqg  3065  csbeq2  3073  csbeq2d  3074  csbnestgf  3101  csbprc  3460  ifbi  3546  pweq  3569  sneq  3594  csbsng  3644  rabsn  3650  dfopg  3763  opeq1  3765  opeq2  3766  csbunig  3804  unieq  3805  inteq  3834  iineq1  3887  iineq2  3890  dfiin2g  3906  iinrabm  3935  iinxprg  3947  opabbid  4054  dcextest  4565  csbxpg  4692  csbdmg  4805  imasng  4976  csbrng  5072  iotaeq  5168  iotabi  5169  dfimafn  5545  fnsnfv  5555  fndmin  5603  fliftf  5778  oprabbid  5906  recseq  6285  freceq1  6371  freceq2  6372  frec0g  6376  freccllem  6381  frecfcllem  6383  frecsuclem  6385  frecsuc  6386  qseq1  6561  qseq2  6562  qsinxp  6589  mapvalg  6636  ixpsnval  6679  ixpeq1  6687  snexxph  6927  fival  6947  prplnqu  7582  cauappcvgprlemlim  7623  caucvgprprlemell  7647  caucvgprprlemelu  7648  caucvgprprlemcbv  7649  caucvgprprlemval  7650  caucvgprprlemnkeqj  7652  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemopu  7661  caucvgprprlemloc  7665  caucvgprprlemclphr  7667  caucvgprprlemexbt  7668  caucvgprprlem1  7671  caucvgprprlem2  7672  caucvgsr  7764  pitonnlem2  7809  pitonn  7810  recidpipr  7818  nntopi  7856  axcaucvglemval  7859  shftlem  10780  shftfibg  10784  shftdm  10786  shftfib  10787  negfi  11191  tgval  12843