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

Theorem elndif 4102
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 4101 . 2 (𝐴 ∈ (𝐶𝐵) → ¬ 𝐴𝐵)
21con2i 141 1 (𝐴𝐵 → ¬ 𝐴 ∈ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2105  cdif 3930
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-dif 3936
This theorem is referenced by:  peano5  7594  extmptsuppeq  7843  undifixp  8486  ssfin4  9720  isf32lem3  9765  isf34lem4  9787  xrinfmss  12691  restntr  21718  cmpcld  21938  reconnlem2  23362  lebnumlem1  23492  i1fd  24209  hgt750lemd  31818  fmlasucdisj  32543  dfon2lem6  32930  onsucconni  33682  meaiininclem  42645  caragendifcl  42673
  Copyright terms: Public domain W3C validator