Theorem abbidv 2196

Description: Equivalent wff's yield equal class abstractions (deduction rule). (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 1461	. 2 |- F/ x ph
2		abbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	abbid 2195	1 |- ( ph -> { x | ps } = { x | ch } )

Syntax hints:   -> wi 4   <-> wb 103   = wceq 1284   {cab 2067

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074

This theorem is referenced by:  cdeqab  2805  csbeq1  2911  sbcel12g  2921  sbceqg  2922  csbeq2d  2930  csbnestgf  2954  csbprc  3289  ifbi  3369  pweq  3385  sneq  3409  csbsng  3453  rabsn  3459  dfopg  3568  opeq1  3570  opeq2  3571  csbunig  3609  unieq  3610  inteq  3639  iineq1  3692  iineq2  3695  dfiin2g  3711  iinrabm  3740  iinxprg  3752  opabbid  3843  csbxpg  4439  csbdmg  4547  imasng  4710  csbrng  4802  iotaeq  4895  iotabi  4896  dfimafn  5243  fnsnfv  5253  fndmin  5295  fliftf  5459  oprabbid  5578  recseq  5944  freceq1  6002  freceq2  6003  frec0g  6006  frecsuclem3  6013  frecsuc  6014  qseq1  6177  qseq2  6178  qsinxp  6205  prplnqu  6810  cauappcvgprlemlim  6851  caucvgprprlemell  6875  caucvgprprlemelu  6876  caucvgprprlemcbv  6877  caucvgprprlemval  6878  caucvgprprlemnkeqj  6880  caucvgprprlemml  6884  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemloc  6893  caucvgprprlemclphr  6895  caucvgprprlemexbt  6896  caucvgprprlem1  6899  caucvgprprlem2  6900  caucvgsr  6978  pitonnlem2  7015  pitonn  7016  recidpipr  7024  nntopi  7060  axcaucvglemval  7063  shftlem  9704  shftfibg  9708  shftdm  9710  shftfib  9711  negfi  10110