Theorem elndif 4156

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979

This theorem is referenced by:  peano5  7932  peano5OLD  7933  extmptsuppeq  8229  undifixp  8992  ssfin4  10379  isf32lem3  10424  isf34lem4  10446  xrinfmss  13372  restntr  23211  cmpcld  23431  reconnlem2  24868  lebnumlem1  25012  i1fd  25735  ssdifidlprm  33451  hgt750lemd  34625  fmlasucdisj  35367  dfon2lem6  35752  onsucconni  36403  meaiininclem  46407  caragendifcl  46435