Theorem eldifi 2214

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 2109	. 2 |- (A e. (B \ C) <-> (A e. B /\ -. A e. C))
2	1	pm3.26bi 320	1 |- (A e. (B \ C) -> A e. B)

Syntax hints:  -. wn 2   -> wi 3   e. wcel 994   \ cdif 2096

This theorem is referenced by:  difss 2219  tz7.7 3001  tfi 3207  peano5 3241  tz7.48-1 4257  tz7.49 4260  pssnn 4681  unblem1 4686  pwfilem 4713  inf3lem3 4760  acdc3lem 7697  acdc2lem1 7700  acdclem 7706  bcthlem33 8242  ablmul 8372  mulid 8373  effoi 9017  strlem1 10458  strlem3 10461  strlem4 10462  strlem5 10463  hstrlem3 10469  hstrlem4 10470  rcfpfillem3 11091  hscptsscld 11491  ist1-2 11603  fimax 11837  recms 12066

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-dif 2101

Copyright terms: Public domain