Theorem elndif 4108

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ∖ cdif 3923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929

This theorem is referenced by:  peano5  7889  extmptsuppeq  8187  undifixp  8948  ssfin4  10324  isf32lem3  10369  isf34lem4  10391  xrinfmss  13326  restntr  23120  cmpcld  23340  reconnlem2  24767  lebnumlem1  24911  i1fd  25634  ssdifidlprm  33473  hgt750lemd  34680  fmlasucdisj  35421  dfon2lem6  35806  onsucconni  36455  meaiininclem  46515  caragendifcl  46543