ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  abbidv Unicode version

Theorem abbidv 2171
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
StepHypRef Expression
1 nfv 1437 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2170 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 102    = wceq 1259   {cab 2042
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049
This theorem is referenced by:  cdeqab  2776  csbeq1  2882  sbcel12g  2892  sbceqg  2893  csbeq2d  2901  csbnestgf  2925  csbprc  3289  ifbi  3375  pweq  3389  sneq  3413  csbsng  3458  rabsn  3464  dfopg  3574  opeq1  3576  opeq2  3577  csbunig  3615  unieq  3616  inteq  3645  iineq1  3698  iineq2  3701  dfiin2g  3717  iinrabm  3746  iinxprg  3758  opabbid  3849  csbxpg  4448  csbdmg  4556  imasng  4717  csbrng  4809  iotaeq  4902  iotabi  4903  dfimafn  5249  fnsnfv  5259  fndmin  5301  fliftf  5466  oprabbid  5585  recseq  5951  freceq1  6009  freceq2  6010  frec0g  6013  frecsuclem3  6020  frecsuc  6021  qseq1  6184  qseq2  6185  qsinxp  6212  prplnqu  6775  cauappcvgprlemlim  6816  caucvgprprlemell  6840  caucvgprprlemelu  6841  caucvgprprlemcbv  6842  caucvgprprlemval  6843  caucvgprprlemnkeqj  6845  caucvgprprlemml  6849  caucvgprprlemmu  6850  caucvgprprlemopl  6852  caucvgprprlemlol  6853  caucvgprprlemopu  6854  caucvgprprlemloc  6858  caucvgprprlemclphr  6860  caucvgprprlemexbt  6861  caucvgprprlem1  6864  caucvgprprlem2  6865  caucvgsr  6943  pitonnlem2  6980  pitonn  6981  recidpipr  6989  nntopi  7025  axcaucvglemval  7028  shftlem  9644  shftfibg  9648  shftdm  9650  shftfib  9651
  Copyright terms: Public domain W3C validator