Theorem eldifi 3255

Description: Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)

Assertion

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

Proof of Theorem eldifi

Step	Hyp	Ref	Expression
1		eldif 3136	. 2 |- ( A e. ( B \ C ) <-> ( A e. B /\ -. A e. C ) )
2	1	simplbi 274	1 |- ( A e. ( B \ C ) -> A e. B )

Syntax hints:   -. wn 3   -> wi 4   e. wcel 2146   \ cdif 3124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-dif 3129

This theorem is referenced by:  difss  3259  ssddif  3367  noel  3424  phpm  6855  fidifsnen  6860  elfi2  6961  fiuni  6967  fifo  6969  fzdifsuc  10049  modfzo0difsn  10363  fsum3cvg  11352  summodclem2a  11355  fisumss  11366  fsumlessfi  11434  binomlem  11457  fproddccvg  11546  prodmodclem2a  11550  fprodssdc  11564  fprodeq0g  11612  fprodmodd  11615  oddprmge3  12100  oddprm  12224  nnoddn2prm  12225  nnoddn2prmb  12227  grpinvnzcl  12801  2irrexpqap  13947  lgslem1  13952  lgslem4  13955  lgsvalmod  13971