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 2106   ∖ cdif 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3951

This theorem is referenced by:  peano5  7883  peano5OLD  7884  extmptsuppeq  8172  undifixp  8927  ssfin4  10304  isf32lem3  10349  isf34lem4  10371  xrinfmss  13288  restntr  22685  cmpcld  22905  reconnlem2  24342  lebnumlem1  24476  i1fd  25197  hgt750lemd  33655  fmlasucdisj  34385  dfon2lem6  34755  onsucconni  35317  meaiininclem  45192  caragendifcl  45220