Theorem eldifi 4140

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2105   ∖ cdif 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965

This theorem is referenced by:  difss  4145  eqoreldif  4689  xpdifid  6189  tz7.7  6411  tfi  7873  peano5  7915  xpord2pred  8168  frrlem12  8320  frrlem13  8321  wfrlem10OLD  8356  wfrlem15OLD  8361  tz7.48-1  8481  tz7.49  8483  dif20el  8541  oaf1o  8599  oeordi  8623  oeord  8624  oecan  8625  oeword  8626  oeworde  8629  oelimcl  8636  oeeulem  8637  oeeui  8638  oaabs2  8685  boxcutc  8979  domdifsn  9092  pssnn  9206  isinf  9293  isinfOLD  9294  pwfilem  9353  fsuppco2  9440  fsuppcor  9441  ordtypelem7  9561  unxpwdom2  9625  inf3lem3  9667  cantnfp1lem1  9715  cantnfp1lem3  9717  ttrcltr  9753  infxpenc2lem1  10056  dfacacn  10179  isf32lem3  10392  isf34lem4  10414  fin67  10432  isfin7-2  10433  domtriomlem  10479  axdc2lem  10485  axdc3lem4  10490  axdc4lem  10492  ttukeylem7  10552  konigthlem  10605  fpwwe2lem12  10679  fpwwe2  10680  modfzo0difsn  13980  hashf1lem1  14490  hashle2prv  14513  rlimrege0  15611  rlimrecl  15612  sumrblem  15743  fsumcvg  15744  summolem2a  15747  fsumss  15757  fsumsplit1  15777  fsumless  15828  cvgcmpce  15850  binomlem  15861  incexclem  15868  incexc  15869  isumltss  15880  prodrblem  15961  fprodcvg  15962  prodmolem2a  15966  fprodss  15980  fprodn0f  16023  fprodeq0g  16026  fprodmodd  16029  rpnnen2lem10  16255  rpnnen2lem11  16256  sumeven  16420  sumodd  16421  lcmfunsnlem2  16673  oddprmge3  16733  oddprm  16843  nnoddn2prm  16844  nnoddn2prmb  16846  iserodd  16868  prmreclem2  16950  prmreclem3  16951  prmreclem5  16953  4sqlem19  16996  prmdvdsprmo  17075  prmodvdslcmf  17080  prmlem0  17139  firest  17478  grpinvnzcl  19041  symgextfv  19450  pmtrf  19487  pmtrdifellem3  19510  sylow2alem2  19650  sylow2a  19651  efgsf  19761  efgsrel  19766  efgs1  19767  efgsfo  19771  gsumzaddlem  19953  gsumzadd  19954  gsumzmhm  19969  gsum2d2lem  20005  dprdfadd  20054  dprdres  20062  subgdmdprd  20068  dmdprdsplitlem  20071  dmdprdsplit2lem  20079  dpjidcl  20092  ablfac1b  20104  pgpfac1lem1  20108  gsummgp0  20331  isirred  20435  irredrmul  20443  ringelnzr  20539  c0rhm  20550  c0rnghm  20551  zrrnghm  20552  zrinitorngc  20658  zrtermorngc  20659  isdomn2  20727  isdomn4  20732  isdrng2  20759  drngmcl  20766  isdrngd  20781  isdrngdOLD  20783  imadrhmcl  20814  cntzsdrg  20819  lcomfsupp  20916  lbspropd  21115  lspsneq  21141  lsppratlem6  21171  lbsextlem2  21178  lbsextlem4  21180  xrs1mnd  21439  xrs10  21440  xrs1cmn  21441  cnsubrg  21462  psgnodpm  21623  zrhpsgnodpm  21627  evpmodpmf1o  21631  uvcresum  21830  frlmssuvc1  21831  frlmsslsp  21833  frlmup2  21836  lindfrn  21858  f1lindf  21859  lindfmm  21864  islindf4  21875  psrbaglesupp  21959  psrlidm  21999  psrridm  22000  mplsubglem  22036  mpllsslem  22037  mplsubrglem  22041  mplmonmul  22071  mplcoe1  22072  mplcoe5  22075  mplbas2  22077  evlslem3  22121  mhpvscacl  22175  psdmul  22187  coe1tmmul2  22294  coe1tmmul  22295  dmatmul  22518  1marepvsma1  22604  mdetdiaglem  22619  mdetrlin  22623  mdetrsca  22624  mdetralt  22629  maducoeval2  22661  madugsum  22664  symgmatr01  22675  gsummatr01lem3  22678  gsummatr01lem4  22679  gsummatr01  22680  smadiadetlem0  22682  smadiadetlem1a  22684  cmpfi  23431  2ndcdisj2  23480  elptr2  23597  ptcnplem  23644  xkopt  23678  kqdisj  23755  fin1aufil  23955  ptcmplem2  24076  ptcmplem3  24077  ptcmplem4  24078  opnsubg  24131  lpbl  24531  blcld  24533  zcld  24848  recld2  24849  reconnlem1  24861  divcnOLD  24903  divcn  24905  iundisj  25596  mbfeqalem1  25689  itg1val2  25732  itg1ge0  25734  i1fmullem  25742  i1fadd  25743  itg1addlem4  25747  itg1addlem4OLD  25748  itg1mulc  25753  itg1lea  25761  itg1le  25762  mbfi1fseqlem4  25767  itg2uba  25792  itg2lea  25793  itg2eqa  25794  itg2splitlem  25797  itg2split  25798  itgeqa  25863  ellimc3  25928  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcobr  25997  dvcobrOLD  25998  dvcjbr  26001  dvrec  26007  dvrecg  26025  dvcnvlem  26028  dvexp3  26030  dveflem  26031  tdeglem4  26113  deg1n0ima  26142  deg1mul3le  26170  ig1peu  26228  ply1termlem  26256  plypf1  26265  plyaddlem1  26266  plymullem1  26267  coeeulem  26277  coeidlem  26290  coeid3  26293  coefv0  26301  coemulhi  26307  coemulc  26308  dvply1  26339  fta1  26364  vieta1lem2  26367  elaa  26372  elqaalem2  26376  aannenlem2  26385  aaliou2  26396  tayl0  26417  dvtaylp  26426  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  pserdvlem2  26486  logbcl  26824  relogbreexp  26832  relogbcxp  26842  cxplogb  26843  dcubic  26903  rlimcnp  27022  jensen  27046  dmgmaddn0  27080  dmlogdmgm  27081  lgamgulmlem2  27087  igamz  27105  gamp1  27115  regamcl  27118  wilthlem2  27126  basellem3  27140  chpub  27278  logexprlim  27283  lgslem1  27355  lgslem4  27358  lgsvalmod  27374  lgsqr  27409  lgsqrmod  27410  lgsqrmodndvds  27411  gausslemma2dlem0b  27415  gausslemma2dlem0c  27416  gausslemma2dlem0i  27422  gausslemma2dlem1a  27423  gausslemma2dlem4  27427  gausslemma2dlem5a  27428  gausslemma2dlem7  27431  gausslemma2d  27432  lgsquad2  27444  m1lgs  27446  2lgsoddprm  27474  2sqreultblem  27506  dchrisum0fno1  27569  rplogsum  27585  ishpg  28781  elntg2  29014  umgrislfupgrlem  29153  usgruspgrb  29214  nbumgrvtx  29377  nbupgrres  29395  isuvtx  29426  cusgrexilem2  29473  cusgrexi  29474  structtocusgr  29477  cusgrres  29480  cusgrfilem2  29488  vtxdginducedm1  29575  cusconngr  30219  2pthfrgr  30312  frgrncvvdeq  30337  frgrwopreglem4  30343  frgrwopreglem5  30349  frgrwopreg  30351  frgrhash2wsp  30360  strlem1  32278  strlem3  32281  strlem4  32282  strlem5  32283  hstrlem3  32289  hstrlem4  32290  iundisjf  32608  suppss3  32741  iundisjfi  32803  suppssnn0  32814  qsdrngi  33502  zringidom  33558  zringfrac  33561  irngnzply1  33705  qtophaus  33796  elzdif0  33942  ind0  33998  measvunilem  34192  sibfof  34321  eulerpartlemb  34349  eulerpartlemf  34351  sseqf  34373  ballotlem5  34480  ballotlemi1  34483  ballotlemii  34484  ballotlemic  34487  ballotlem1c  34488  ballotlemscr  34499  ballotlemro  34503  ballotlemfg  34506  ballotlemfrc  34507  ballotlemfrceq  34509  ballotlemrinv0  34513  plymulx0  34540  signstfvn  34562  signsvfn  34575  bnj923  34760  bnj570  34897  bnj594  34904  subfacp1lem1  35163  satffunlem2lem1  35388  mrsubcn  35503  mrsubco  35505  circum  35658  dfon2lem6  35769  neibastop1  36341  bj-restn0b  37073  lindsadd  37599  lindsenlbs  37601  matunitlindflem1  37602  poimirlem24  37630  poimirlem25  37631  dvtan  37656  itg2addnclem2  37658  ftc1cnnc  37678  dvasin  37690  dvreasin  37692  dvreacos  37693  isdrngo2  37944  isdrngo3  37945  divrngidl  38014  isfldidl  38054  pridlc2  38058  pridlc3  38059  prter2  38862  lsateln0  38976  lsatlss  38977  lsmsat  38989  lsatcv0  39012  lsat0cv  39014  lcv1  39022  l1cvpat  39035  dih1dimatlem  41311  dihatexv2  41321  djhcvat42  41397  dihjat1lem  41410  dochsatshp  41433  lcfl6  41482  mapdrvallem2  41627  mapdpglem32  41687  idomnnzgmulnz  42114  aks6d1c5lem3  42118  aks6d1c5lem2  42119  deg1gprod  42121  sticksstones22  42149  unitscyglem4  42179  readvrec2  42369  readvrec  42370  evlsvvvallem  42547  evlsvvvallem2  42548  evlsvvval  42549  evlsbagval  42552  selvvvval  42571  evlselv  42573  evlsmhpvvval  42581  prjspertr  42591  prjsperref  42592  prjspersym  42593  prjspvs  42596  prjsprellsp  42597  dffltz  42620  irrapx1  42815  pell1234qrne0  42840  pell1234qrreccl  42841  pell1234qrmulcl  42842  pell14qrgt0  42846  pell1234qrdich  42848  pell14qrdich  42856  pell1qrge1  42857  pell1qr1  42858  pell1qrgap  42861  pell14qrgapw  42863  pellqrexplicit  42864  pellqrex  42866  pellfundge  42869  pellfundgt1  42870  setindtr  43012  kelac1  43051  mpaaeu  43138  flcidc  43158  deg1mhm  43188  onexoegt  43232  cantnfub  43310  cantnfresb  43313  succlg  43317  dflim5  43318  onmcl  43320  omabs2  43321  tfsconcatrev  43337  minregex2  43524  radcnvrat  44309  binomcxplemdvbinom  44348  disjiun2  44997  fiiuncl  45004  disjf1o  45133  difmapsn  45154  supminfxr2  45418  icoiccdif  45476  iccdificc  45491  fsumnncl  45527  fsumsupp0  45533  fprod0  45551  climrec  45558  islpcn  45594  lptre2pt  45595  limclner  45606  cnrefiisplem  45784  fprodcncf  45855  fperdvper  45874  dvdivcncf  45882  dvnmul  45898  dvmptfprodlem  45899  dvnprodlem2  45902  stoweidlem25  45980  stoweidlem28  45983  stoweidlem41  45996  stoweidlem44  45999  stoweidlem46  46001  stirlinglem5  46033  dirkercncflem1  46058  dirkercncflem2  46059  fourierdlem24  46086  fourierdlem62  46123  fouriersw  46186  fouriercn  46187  elaa2lem  46188  elaa2  46189  etransclem25  46214  etransclem35  46224  etransclem44  46233  sge0iunmptlemfi  46368  sge0fodjrnlem  46371  iundjiunlem  46414  meadjiunlem  46420  meaiininclem  46441  isomenndlem  46485  hsphoidmvle2  46540  hsphoidmvle  46541  hoidmv1lelem2  46547  hoidmvle  46555  ovnhoilem1  46556  hspdifhsp  46571  hspmbllem2  46582  ovnsubadd2lem  46600  ovolval4lem1  46604  preimagelt  46654  preimalegt  46655  fsummsndifre  47296  fsummmodsndifre  47298  odz2prm2pw  47487  fmtnoprmfac1lem  47488  fmtnoprmfac2lem1  47490  2pwp1prm  47513  lighneallem2  47530  lighneallem3  47531  lighneallem4  47534  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbndlem4  47732  bgoldbtbnd  47733  isubgrvtxuhgr  47787  2zrngnmlid2  48100  mgpsumunsn  48205  mgpsumz  48206  mgpsumn  48207  lindslinindsimp1  48302  lindslinindsimp2  48308  lincresunit1  48322  lincresunit2  48323  lincresunit3lem1  48324  lincresunit3lem2  48325  lincresunit3  48326  lindssnlvec  48331  logcxp0  48384  relogbmulbexp  48410  relogbdivb  48411  dignn0fr  48450  rrxlinesc  48584  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587