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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902

This theorem is used by:  peano5  7890  extmptsuppeq  8186  undifixp  8941  ssfin4  10312  isf32lem3  10357  isf34lem4  10379  xrinfmss  13362  ssdifidlprm  21549  restntr  23407  cmpcld  23627  reconnlem2  25054  lebnumlem1  25189  i1fd  25909  plngrotlem1  29144  plngrotlem2  29145  dflringlem3  33906  dflring3  33907  dflring4  33908  hgt750lemd  35156  fmlasucdisj  35978  dfon2lem6  36365  onsucconni  37056  meaiininclem  47314  caragendifcl  47342