Theorem elndif 4068

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4046

This theorem is used by:  peano5  7909  extmptsuppeq  8212  undifixp  8969  ssfin4  10395  isf32lem3  10440  isf34lem4  10462  xrinfmss  13447  ssdifidlprm  21651  restntr  23509  cmpcld  23729  reconnlem2  25156  lebnumlem1  25291  i1fd  26011  plngrotlem1  29274  plngrotlem2  29275  dflringlem3  34078  dflring3  34079  dflring4  34080  hgt750lemd  35327  fmlasucdisj  36254  dfon2lem6  36646  onsucconni  37321  meaiininclem  47604  caragendifcl  47632