Theorem eldifi 2162

Description: Implication of membership in a class difference.

Assertion

Ref	Expression
eldifi	|- (A e. (B \ C) -> A e. B)

Proof of Theorem eldifi

Step	Hyp	Ref	Expression
1		eldif 2057	. 2 |- (A e. (B \ C) <-> (A e. B /\ -. A e. C))
2	1	pm3.26bi 322	1 |- (A e. (B \ C) -> A e. B)

Syntax hints:  -. wn 2   -> wi 3   e. wcel 958   \ cdif 2044

This theorem is referenced by:  difss 2167  tz7.7 2973  tfi 3126  peano5 3153  tz7.48-1 3956  tz7.49 3959  pssnn 4534  unblem1 4540  pwfilemOLD 4570  inf3lem3 4615  acdc3lem 7486  acdc2lem1 7488  acdclem 7494  bcthlem33 8031  ablmul 8131  mulid 8132  effoi 8745  strlem1 10177  strlem3 10180  strlem4 10181  strlem5 10182  hstrlem3 10188  hstrlem4 10189  rcfpfillem3 10589  rcfpfillem3OLD 10590

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-dif 2049

Copyright terms: Public domain