Theorem elndif 4080

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

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

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902

This theorem is used by:  peano5  7903  extmptsuppeq  8198  undifixp  8955  ssfin4  10381  isf32lem3  10426  isf34lem4  10448  xrinfmss  13433  ssdifidlprm  21635  restntr  23493  cmpcld  23713  reconnlem2  25140  lebnumlem1  25275  i1fd  25995  plngrotlem1  29258  plngrotlem2  29259  dflringlem3  34021  dflring3  34022  dflring4  34023  hgt750lemd  35270  fmlasucdisj  36143  dfon2lem6  36530  onsucconni  37205  meaiininclem  47465  caragendifcl  47493