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

Theorem eldifsn 3523
Description: Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
Assertion
Ref Expression
eldifsn (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))

Proof of Theorem eldifsn
StepHypRef Expression
1 eldif 2955 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2 elsng 3418 . . . 4 (𝐴𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
32necon3bbid 2260 . . 3 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴𝐶))
43pm5.32i 435 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
51, 4bitri 177 1 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 101  wb 102  wcel 1409  wne 2220  cdif 2942  {csn 3403
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-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  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  df-clel 2052  df-nfc 2183  df-ne 2221  df-v 2576  df-dif 2948  df-sn 3409
This theorem is referenced by:  eldifsni  3524  rexdifsn  3527  difsn  3529  fnniniseg2  5318  rexsupp  5319  suppssfv  5736  suppssov1  5737  dif1o  6052  fidifsnen  6362  elni  6464  divvalap  7727  elnnne0  8253  divfnzn  8653  modfzo0difsn  9345  modsumfzodifsn  9346  fzo0dvdseq  10169
  Copyright terms: Public domain W3C validator