Theorem eldifi 3329

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 3209	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ 𝐶))
2	1	simplbi 274	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2202   ∖ cdif 3197

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-dif 3202

This theorem is referenced by:  difss  3333  ssddif  3441  noel  3498  phpm  7051  fidifsnen  7056  elfi2  7170  fiuni  7176  fifo  7178  fzdifsuc  10315  modfzo0difsn  10656  fsum3cvg  11938  summodclem2a  11941  fisumss  11952  fsumlessfi  12020  binomlem  12043  fproddccvg  12132  prodmodclem2a  12136  fprodssdc  12150  fprodeq0g  12198  fprodmodd  12201  oddprmge3  12706  oddprm  12831  nnoddn2prm  12832  nnoddn2prmb  12834  4sqlem19  12981  grpinvnzcl  13654  ringelnzr  14200  ply1termlem  15465  plyaddlem1  15470  plymullem1  15471  plycoeid3  15480  dvply1  15488  2irrexpqap  15701  lgslem1  15728  lgslem4  15731  lgsvalmod  15747  gausslemma2dlem0b  15778  gausslemma2dlem0c  15779  gausslemma2dlem1a  15786  gausslemma2dlem1cl  15787  gausslemma2dlem1f1o  15788  gausslemma2dlem4  15792  gausslemma2d  15797  lgsquad2  15811  m1lgs  15813  2lgsoddprm  15841