Theorem elndif 4087

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

Step	Hyp	Ref	Expression
1		eldifn 4086	. 2 ⊢ (𝐴 ∈ (𝐶 ∖ 𝐵) → ¬ 𝐴 ∈ 𝐵)
2	1	con2i 140	1 ⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2143   ∖ cdif 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908

This theorem is referenced by:  peano5  7886  extmptsuppeq  8180  undifixp  8928  ssfin4  10289  isf32lem3  10334  isf34lem4  10356  xrinfmss  13331  ssdifidlprm  21486  restntr  23339  cmpcld  23559  reconnlem2  24985  lebnumlem1  25120  i1fd  25840  plngrotlem1  29069  plngrotlem2  29070  dflringlem3  33786  dflring3  33787  dflring4  33788  hgt750lemd  35035  fmlasucdisj  35891  dfon2lem6  36278  onsucconni  36948  meaiininclem  47200  caragendifcl  47228