Theorem elndif 4128

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2105   ∖ cdif 3945

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-dif 3951

This theorem is referenced by:  peano5  7888  peano5OLD  7889  extmptsuppeq  8177  undifixp  8932  ssfin4  10309  isf32lem3  10354  isf34lem4  10376  xrinfmss  13294  restntr  22907  cmpcld  23127  reconnlem2  24564  lebnumlem1  24708  i1fd  25431  hgt750lemd  33959  fmlasucdisj  34689  dfon2lem6  35065  onsucconni  35626  meaiininclem  45501  caragendifcl  45529