MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elndif Structured version   Visualization version   GIF version

Theorem elndif 3930
Description: A set does not belong to a class excluding it. (Contributed by NM, 27-Jun-1994.)
Assertion
Ref Expression
elndif (𝐴𝐵 → ¬ 𝐴 ∈ (𝐶𝐵))

Proof of Theorem elndif
StepHypRef Expression
1 eldifn 3929 . 2 (𝐴 ∈ (𝐶𝐵) → ¬ 𝐴𝐵)
21con2i 137 1 (𝐴𝐵 → ¬ 𝐴 ∈ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2157  cdif 3764
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-v 3385  df-dif 3770
This theorem is referenced by:  peano5  7321  extmptsuppeq  7554  undifixp  8182  ssfin4  9418  isf32lem3  9463  isf34lem4  9485  xrinfmss  12385  restntr  21312  cmpcld  21531  reconnlem2  22955  lebnumlem1  23085  i1fd  23786  hgt750lemd  31238  dfon2lem6  32197  onsucconni  32936  meaiininclem  41434  caragendifcl  41462
  Copyright terms: Public domain W3C validator