Theorem eldifi 3326

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 3206	. 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 2200   \ cdif 3194

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-dif 3199

This theorem is referenced by:  difss  3330  ssddif  3438  noel  3495  phpm  7035  fidifsnen  7040  elfi2  7150  fiuni  7156  fifo  7158  fzdifsuc  10289  modfzo0difsn  10629  fsum3cvg  11905  summodclem2a  11908  fisumss  11919  fsumlessfi  11987  binomlem  12010  fproddccvg  12099  prodmodclem2a  12103  fprodssdc  12117  fprodeq0g  12165  fprodmodd  12168  oddprmge3  12673  oddprm  12798  nnoddn2prm  12799  nnoddn2prmb  12801  4sqlem19  12948  grpinvnzcl  13621  ringelnzr  14167  ply1termlem  15432  plyaddlem1  15437  plymullem1  15438  plycoeid3  15447  dvply1  15455  2irrexpqap  15668  lgslem1  15695  lgslem4  15698  lgsvalmod  15714  gausslemma2dlem0b  15745  gausslemma2dlem0c  15746  gausslemma2dlem1a  15753  gausslemma2dlem1cl  15754  gausslemma2dlem1f1o  15755  gausslemma2dlem4  15759  gausslemma2d  15764  lgsquad2  15778  m1lgs  15780  2lgsoddprm  15808