Theorem eldifi 3269

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

Assertion

Ref	Expression
eldifi	⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵)

Proof of Theorem eldifi

Step	Hyp	Ref	Expression
1		eldif 3150	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
2	1	simplbi 274	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2158   ∖ cdif 3138

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 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-dif 3143

This theorem is referenced by:  difss  3273  ssddif  3381  noel  3438  phpm  6879  fidifsnen  6884  elfi2  6985  fiuni  6991  fifo  6993  fzdifsuc  10095  modfzo0difsn  10409  fsum3cvg  11400  summodclem2a  11403  fisumss  11414  fsumlessfi  11482  binomlem  11505  fproddccvg  11594  prodmodclem2a  11598  fprodssdc  11612  fprodeq0g  11660  fprodmodd  11663  oddprmge3  12149  oddprm  12273  nnoddn2prm  12274  nnoddn2prmb  12276  grpinvnzcl  12969  ringelnzr  13407  2irrexpqap  14692  lgslem1  14697  lgslem4  14700  lgsvalmod  14716  m1lgs  14748