Theorem abbidv 2358

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

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1402   {cab 2224

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231

This theorem is referenced by:  rabbidva2  2805  cdeqab  3041  sbceqbid  3058  csbeq1  3150  sbcel12g  3162  sbceqg  3163  csbeq2  3171  csbeq2d  3172  csbnestgf  3200  csbprc  3571  ifbi  3658  pweq  3688  sneq  3716  csbsng  3766  rabsn  3772  dfopg  3897  opeq1  3899  opeq2  3900  csbunig  3938  unieq  3939  inteq  3968  iineq1  4021  iineq2  4024  dfiin2g  4040  iinrabm  4070  iinxprg  4082  opabbid  4191  dcextest  4723  csbxpg  4851  csbdmg  4970  imasng  5147  csbrng  5244  iotaeq  5341  iotabi  5342  dfimafn  5745  fnsnfv  5756  fndmin  5807  dfimafnf  5945  fliftf  5995  oprabbid  6131  recseq  6567  freceq1  6653  freceq2  6654  frec0g  6658  freccllem  6663  frecfcllem  6665  frecsuclem  6667  frecsuc  6668  qseq1  6847  qseq2  6848  qsinxp  6875  mapvalg  6922  ixpsnval  6973  ixpeq1  6981  snexxph  7257  fival  7294  acneq  7548  prplnqu  7977  cauappcvgprlemlim  8018  caucvgprprlemell  8042  caucvgprprlemelu  8043  caucvgprprlemcbv  8044  caucvgprprlemval  8045  caucvgprprlemnkeqj  8047  caucvgprprlemml  8051  caucvgprprlemmu  8052  caucvgprprlemopl  8054  caucvgprprlemlol  8055  caucvgprprlemopu  8056  caucvgprprlemloc  8060  caucvgprprlemclphr  8062  caucvgprprlemexbt  8063  caucvgprprlem1  8066  caucvgprprlem2  8067  caucvgsr  8159  pitonnlem2  8204  pitonn  8205  recidpipr  8213  nntopi  8251  axcaucvglemval  8254  hashf1lem2  11264  hashf1  11265  hashfac  11266  csbwrdg  11312  shftlem  11559  shftfibg  11563  shftdm  11565  shftfib  11566  negfi  11972  tgval  13593  ptex  13595  eqglact  14005  isghm  14023  ixpsnbasval  14775  plyval  15756  vtxdfifiun  16452