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 ⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2146   ∖ cdif 3903

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909

This theorem is used by:  peano5  7892  extmptsuppeq  8186  undifixp  8934  ssfin4  10305  isf32lem3  10350  isf34lem4  10372  xrinfmss  13348  ssdifidlprm  21516  restntr  23369  cmpcld  23589  reconnlem2  25016  lebnumlem1  25151  i1fd  25871  plngrotlem1  29100  plngrotlem2  29101  dflringlem3  33826  dflring3  33827  dflring4  33828  hgt750lemd  35076  fmlasucdisj  35904  dfon2lem6  36291  onsucconni  36981  meaiininclem  47233  caragendifcl  47261