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

Theorem eldifsn 3620
Description: Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
Assertion
Ref Expression
eldifsn  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )

Proof of Theorem eldifsn
StepHypRef Expression
1 eldif 3050 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsng 3512 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2325 . . 3  |-  ( A  e.  B  ->  ( -.  A  e.  { C } 
<->  A  =/=  C ) )
43pm5.32i 449 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
51, 4bitri 183 1  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 103    <-> wb 104    e. wcel 1465    =/= wne 2285    \ cdif 3038   {csn 3497
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-in1 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-v 2662  df-dif 3043  df-sn 3503
This theorem is referenced by:  eldifsni  3622  rexdifsn  3625  difsn  3627  fnniniseg2  5511  rexsupp  5512  mpodifsnif  5832  suppssfv  5946  suppssov1  5947  dif1o  6303  fidifsnen  6732  en2eleq  7019  en2other2  7020  elni  7084  divvalap  8402  elnnne0  8959  divfnzn  9381  modfzo0difsn  10136  modsumfzodifsn  10137  hashdifpr  10534  eff2  11313  tanvalap  11342  fzo0dvdseq  11482  oddprmgt2  11741  setsslnid  11937
  Copyright terms: Public domain W3C validator