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

Theorem elndif 4109
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 4108 . 2 (𝐴 ∈ (𝐶𝐵) → ¬ 𝐴𝐵)
21con2i 141 1 (𝐴𝐵 → ¬ 𝐴 ∈ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2107  cdif 3937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-dif 3943
This theorem is referenced by:  peano5  7593  extmptsuppeq  7845  undifixp  8487  ssfin4  9721  isf32lem3  9766  isf34lem4  9788  xrinfmss  12693  restntr  21709  cmpcld  21929  reconnlem2  23353  lebnumlem1  23483  i1fd  24200  hgt750lemd  31808  fmlasucdisj  32533  dfon2lem6  32920  onsucconni  33672  meaiininclem  42637  caragendifcl  42665
  Copyright terms: Public domain W3C validator