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  7052  fidifsnen  7057  elfi2  7171  fiuni  7177  fifo  7179  fzdifsuc  10316  modfzo0difsn  10658  fsum3cvg  11957  summodclem2a  11960  fisumss  11971  fsumlessfi  12039  binomlem  12062  fproddccvg  12151  prodmodclem2a  12155  fprodssdc  12169  fprodeq0g  12217  fprodmodd  12220  oddprmge3  12725  oddprm  12850  nnoddn2prm  12851  nnoddn2prmb  12853  4sqlem19  13000  grpinvnzcl  13673  ringelnzr  14220  ply1termlem  15485  plyaddlem1  15490  plymullem1  15491  plycoeid3  15500  dvply1  15508  2irrexpqap  15721  lgslem1  15748  lgslem4  15751  lgsvalmod  15767  gausslemma2dlem0b  15798  gausslemma2dlem0c  15799  gausslemma2dlem1a  15806  gausslemma2dlem1cl  15807  gausslemma2dlem1f1o  15808  gausslemma2dlem4  15812  gausslemma2d  15817  lgsquad2  15831  m1lgs  15833  2lgsoddprm  15861