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

Theorem elndif 4129
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 4128 . 2 (𝐴 ∈ (𝐶𝐵) → ¬ 𝐴𝐵)
21con2i 139 1 (𝐴𝐵 → ¬ 𝐴 ∈ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2107  cdif 3946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952
This theorem is referenced by:  peano5  7884  peano5OLD  7885  extmptsuppeq  8173  undifixp  8928  ssfin4  10305  isf32lem3  10350  isf34lem4  10372  xrinfmss  13289  restntr  22686  cmpcld  22906  reconnlem2  24343  lebnumlem1  24477  i1fd  25198  hgt750lemd  33660  fmlasucdisj  34390  dfon2lem6  34760  onsucconni  35322  meaiininclem  45202  caragendifcl  45230
  Copyright terms: Public domain W3C validator