Theorem elndif 4095

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2149   ∖ cdif 3910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916

This theorem is referenced by:  peano5  7886  extmptsuppeq  8180  undifixp  8928  ssfin4  10290  isf32lem3  10335  isf34lem4  10357  xrinfmss  13332  ssdifidlprm  21451  restntr  23304  cmpcld  23524  reconnlem2  24950  lebnumlem1  25085  i1fd  25805  plngrotlem1  29023  plngrotlem2  29024  dflringlem3  33727  dflring3  33728  dflring4  33729  hgt750lemd  34976  fmlasucdisj  35786  dfon2lem6  36173  onsucconni  36833  meaiininclem  47085  caragendifcl  47113