Theorem elndif 4084

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 4083	. 2 ⊢ (𝐴 ∈ (𝐶 ∖ 𝐵) → ¬ 𝐴 ∈ 𝐵)
2	1	con2i 139	1 ⊢ (𝐴 ∈ 𝐵 → ¬ 𝐴 ∈ (𝐶 ∖ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2141   ∖ cdif 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3905

This theorem is referenced by:  peano5  7869  extmptsuppeq  8162  undifixp  8910  ssfin4  10261  isf32lem3  10306  isf34lem4  10328  xrinfmss  13307  restntr  23230  cmpcld  23450  reconnlem2  24876  lebnumlem1  25011  i1fd  25731  ssdifidlprm  33606  dflringlem3  33653  dflring3  33654  dflring4  33655  hgt750lemd  34903  fmlasucdisj  35710  dfon2lem6  36097  onsucconni  36758  meaiininclem  47021  caragendifcl  47049