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

Theorem elndif 3883
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 3882 . 2 (𝐴 ∈ (𝐶𝐵) → ¬ 𝐴𝐵)
21con2i 136 1 (𝐴𝐵 → ¬ 𝐴 ∈ (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2144  cdif 3718
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-dif 3724
This theorem is referenced by:  peano5  7235  extmptsuppeq  7469  undifixp  8097  ssfin4  9333  isf32lem3  9378  isf34lem4  9400  xrinfmss  12344  restntr  21206  cmpcld  21425  reconnlem2  22849  lebnumlem1  22979  i1fd  23667  hgt750lemd  31060  dfon2lem6  32023  onsucconni  32767  meaiininclem  41214  caragendifcl  41242
  Copyright terms: Public domain W3C validator