Theorem elndif 4085

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113   ∖ cdif 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904

This theorem is referenced by:  peano5  7835  extmptsuppeq  8130  undifixp  8872  ssfin4  10220  isf32lem3  10265  isf34lem4  10287  xrinfmss  13225  restntr  23126  cmpcld  23346  reconnlem2  24772  lebnumlem1  24916  i1fd  25638  ssdifidlprm  33539  hgt750lemd  34805  fmlasucdisj  35593  dfon2lem6  35980  onsucconni  36631  meaiininclem  46730  caragendifcl  46758