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

Theorem abbidv 2200
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 1462 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2199 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 103    = wceq 1285   {cab 2069
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076
This theorem is referenced by:  cdeqab  2814  csbeq1  2920  sbcel12g  2930  sbceqg  2931  csbeq2d  2939  csbnestgf  2963  csbprc  3305  ifbi  3386  pweq  3403  sneq  3427  csbsng  3471  rabsn  3477  dfopg  3588  opeq1  3590  opeq2  3591  csbunig  3629  unieq  3630  inteq  3659  iineq1  3712  iineq2  3715  dfiin2g  3731  iinrabm  3760  iinxprg  3772  opabbid  3863  csbxpg  4467  csbdmg  4577  imasng  4740  csbrng  4832  iotaeq  4925  iotabi  4926  dfimafn  5275  fnsnfv  5285  fndmin  5327  fliftf  5491  oprabbid  5610  recseq  5976  freceq1  6062  freceq2  6063  frec0g  6067  freccllem  6072  frecfcllem  6074  frecsuclem  6076  frecsuc  6077  qseq1  6242  qseq2  6243  qsinxp  6270  prplnqu  6942  cauappcvgprlemlim  6983  caucvgprprlemell  7007  caucvgprprlemelu  7008  caucvgprprlemcbv  7009  caucvgprprlemval  7010  caucvgprprlemnkeqj  7012  caucvgprprlemml  7016  caucvgprprlemmu  7017  caucvgprprlemopl  7019  caucvgprprlemlol  7020  caucvgprprlemopu  7021  caucvgprprlemloc  7025  caucvgprprlemclphr  7027  caucvgprprlemexbt  7028  caucvgprprlem1  7031  caucvgprprlem2  7032  caucvgsr  7110  pitonnlem2  7147  pitonn  7148  recidpipr  7156  nntopi  7192  axcaucvglemval  7195  shftlem  9923  shftfibg  9927  shftdm  9929  shftfib  9930  negfi  10329
  Copyright terms: Public domain W3C validator