Theorem eldifi 4086

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2144   ∖ cdif 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-dif 3909

This theorem is referenced by:  difss  4091  eqoreldif  4646  xpdifid  6155  xpdifcnvepel  6156  tz7.7  6374  tfi  7835  peano5  7876  resf1extb  7917  resf1ext2b  7918  xpord2pred  8127  frrlem12  8280  frrlem13  8281  tz7.48-1  8416  tz7.49  8418  dif20el  8476  oaf1o  8534  oeordi  8559  oeord  8560  oecan  8561  oeword  8562  oeworde  8565  oelimcl  8572  oeeulem  8573  oeeui  8574  oaabs2  8621  boxcutc  8925  domdifsn  9034  pssnn  9139  isinf  9211  pwfilem  9264  fsuppco2  9351  fsuppcor  9352  ordtypelem7  9474  unxpwdom2  9538  inf3lem3  9587  cantnfp1lem1  9635  cantnfp1lem3  9637  ttrcltr  9673  infxpenc2lem1  9977  dfacacn  10100  isf32lem3  10314  isf34lem4  10336  fin67  10354  isfin7-2  10355  domtriomlem  10401  axdc2lem  10407  axdc3lem4  10412  axdc4lem  10414  ttukeylem7  10474  konigthlem  10528  fpwwe2lem12  10602  fpwwe2  10603  ind0  12207  modfzo0difsn  13958  hashf1lem1  14470  hashle2prv  14493  rlimrege0  15608  rlimrecl  15609  sumrblem  15740  fsumcvg  15741  summolem2a  15744  fsumss  15754  fsumsplit1  15774  fsumless  15826  cvgcmpce  15848  binomlem  15861  incexclem  15868  incexc  15869  isumltss  15880  prodrblem  15961  fprodcvg  15962  prodmolem2a  15966  fprodss  15980  fprodn0f  16023  fprodeq0g  16026  fprodmodd  16029  rpnnen2lem10  16257  rpnnen2lem11  16258  sumeven  16423  sumodd  16424  lcmfunsnlem2  16676  oddprmge3  16737  oddprm  16848  nnoddn2prm  16849  nnoddn2prmb  16851  iserodd  16873  prmreclem2  16955  prmreclem3  16956  prmreclem5  16958  4sqlem19  17001  prmdvdsprmo  17080  prmodvdslcmf  17085  prmlem0  17143  firest  17463  chnccat  18660  chnrev  18661  grpinvnzcl  19055  symgextfv  19460  pmtrf  19497  pmtrdifellem3  19520  sylow2alem2  19660  sylow2a  19661  efgsf  19771  efgsrel  19776  efgs1  19777  efgsfo  19781  gsumzaddlem  19963  gsumzadd  19964  gsumzmhm  19979  gsum2d2lem  20015  dprdfadd  20064  dprdres  20072  subgdmdprd  20078  dmdprdsplitlem  20081  dmdprdsplit2lem  20089  dpjidcl  20102  ablfac1b  20114  pgpfac1lem1  20118  gsummgp0  20368  isirred  20470  irredrmul  20478  ringelnzr  20575  c0rhm  20586  c0rnghm  20587  zrrnghm  20588  zrinitorngc  20694  zrtermorngc  20695  isdomn2  20763  isdomn4  20768  isdrng2  20795  drngmcl  20802  isdrngd  20817  isdrngdOLD  20819  imadrhmcl  20848  cntzsdrg  20853  lcomfsupp  20971  lbspropd  21168  lspsneq  21194  lsppratlem6  21224  lbsextlem2  21231  lbsextlem4  21233  cnsubrg  21481  xrs1mnd  21494  xrs10  21495  xrs1cmn  21496  psgnodpm  21642  zrhpsgnodpm  21646  evpmodpmf1o  21650  uvcresum  21847  frlmssuvc1  21848  frlmsslsp  21850  frlmup2  21853  lindfrn  21875  f1lindf  21876  lindfmm  21881  islindf4  21892  psrbaglesupp  21976  psrlidm  22015  psrridm  22016  mplsubglem  22052  mpllsslem  22053  mplsubrglem  22057  mplmonmul  22091  mplcoe1  22092  mplcoe5  22095  mplbas2  22097  evlslem3  22135  evlsvvvallem  22146  evlsvvvallem2  22147  evlsvvval  22148  selvvvval  22197  mhpvscacl  22221  psdmul  22233  coe1tmmul2  22341  coe1tmmul  22342  dmatmul  22559  1marepvsma1  22645  mdetdiaglem  22660  mdetrlin  22664  mdetrsca  22665  mdetralt  22670  maducoeval2  22702  madugsum  22705  symgmatr01  22716  gsummatr01lem3  22719  gsummatr01lem4  22720  gsummatr01  22721  smadiadetlem0  22723  smadiadetlem1a  22725  cmpfi  23470  2ndcdisj2  23519  elptr2  23636  ptcnplem  23683  xkopt  23717  kqdisj  23794  fin1aufil  23994  ptcmplem2  24115  ptcmplem3  24116  ptcmplem4  24117  opnsubg  24170  lpbl  24565  blcld  24567  zcld  24876  recld2  24877  reconnlem1  24889  divcn  24932  iundisj  25612  mbfeqalem1  25705  itg1val2  25748  itg1ge0  25750  i1fmullem  25758  i1fadd  25759  itg1addlem4  25763  itg1mulc  25768  itg1lea  25776  itg1le  25777  mbfi1fseqlem4  25782  itg2uba  25807  itg2lea  25808  itg2eqa  25809  itg2splitlem  25812  itg2split  25813  itgeqa  25878  ellimc3  25943  dvaddbr  26002  dvmulbr  26003  dvcobr  26010  dvcjbr  26013  dvrec  26019  dvrecg  26037  dvcnvlem  26040  dvexp3  26042  dveflem  26043  tdeglem4  26122  deg1n0ima  26151  deg1mul3le  26179  ig1peu  26237  ply1termlem  26265  plypf1  26274  plyaddlem1  26275  plymullem1  26276  coeeulem  26286  coeidlem  26299  coeid3  26302  coefv0  26310  coemulhi  26316  coemulc  26317  plyn0mulidp  26347  dvply1  26350  fta1  26374  vieta1lem2  26377  elaa  26382  elqaalem2  26386  aannenlem2  26395  aaliou2  26406  tayl0  26427  dvtaylp  26435  taylthlem1  26438  taylthlem2  26439  pserdvlem2  26493  logbcl  26834  relogbreexp  26842  relogbcxp  26852  cxplogb  26853  dcubic  26913  rlimcnp  27032  jensen  27055  dmgmaddn0  27089  dmlogdmgm  27090  lgamgulmlem2  27096  igamz  27114  gamp1  27124  regamcl  27127  wilthlem2  27135  basellem3  27149  chpub  27286  logexprlim  27291  lgslem1  27363  lgslem4  27366  lgsvalmod  27382  lgsqr  27417  lgsqrmod  27418  lgsqrmodndvds  27419  gausslemma2dlem0b  27423  gausslemma2dlem0c  27424  gausslemma2dlem0i  27430  gausslemma2dlem1a  27431  gausslemma2dlem4  27435  gausslemma2dlem5a  27436  gausslemma2dlem7  27439  gausslemma2d  27440  lgsquad2  27452  m1lgs  27454  2lgsoddprm  27482  2sqreultblem  27514  dchrisum0fno1  27577  rplogsum  27593  ishpg  28934  elntg2  29188  umgrislfupgrlem  29325  usgruspgrb  29386  nbumgrvtx  29549  nbupgrres  29567  isuvtx  29598  cusgrexilem2  29645  cusgrexi  29646  structtocusgr  29649  cusgrres  29651  cusgrfilem2  29659  vtxdginducedm1  29746  cusconngr  30395  2pthfrgr  30488  frgrncvvdeq  30513  frgrwopreglem4  30519  frgrwopreglem5  30525  frgrwopreg  30527  frgrhash2wsp  30536  strlem1  32455  strlem3  32458  strlem4  32459  strlem5  32460  hstrlem3  32466  hstrlem4  32467  iundisjf  32791  suppss3  32927  iundisjfi  33000  suppssnn0  33009  qsdrngi  33685  zringidom  33749  zringfrac  33752  psrmonmul  33849  irngnzply1  33990  qtophaus  34135  elzdif0  34279  measvunilem  34511  sibfof  34639  eulerpartlemb  34667  eulerpartlemf  34669  sseqf  34691  ballotlem5  34799  ballotlemi1  34802  ballotlemii  34803  ballotlemic  34806  ballotlem1c  34807  ballotlemscr  34818  ballotlemro  34822  ballotlemfg  34825  ballotlemfrc  34826  ballotlemfrceq  34828  ballotlemrinv0  34832  signstfvn  34865  signsvfn  34878  bnj923  35066  bnj570  35202  bnj594  35209  fineqvnttrclselem1  35421  fineqvnttrclselem2  35422  fineqvnttrclselem3  35423  fineqvnttrclse  35424  subfacp1lem1  35534  satffunlem2lem1  35759  mrsubcn  35874  mrsubco  35876  circum  36029  dfon2lem6  36141  neibastop1  36724  bj-restn0b  37586  lindsadd  38117  lindsenlbs  38119  matunitlindflem1  38120  poimirlem24  38148  poimirlem25  38149  dvtan  38174  itg2addnclem2  38176  ftc1cnnc  38196  dvasin  38208  dvreasin  38210  dvreacos  38211  isdrngo2  38462  isdrngo3  38463  divrngidl  38532  isfldidl  38572  pridlc2  38576  pridlc3  38577  blockadjliftmap  38962  prter2  39510  lsateln0  39624  lsatlss  39625  lsmsat  39637  lsatcv0  39660  lsat0cv  39662  lcv1  39670  l1cvpat  39683  dih1dimatlem  41958  dihatexv2  41968  djhcvat42  42044  dihjat1lem  42057  dochsatshp  42080  lcfl6  42129  mapdrvallem2  42274  mapdpglem32  42334  idomnnzgmulnz  42755  aks6d1c5lem3  42759  aks6d1c5lem2  42760  deg1gprod  42762  sticksstones22  42790  unitscyglem4  42820  readvrec2  42975  readvrec  42976  readvcot  42978  evlsbagval  43173  evlselv  43176  evlsmhpvvval  43182  prjspertr  43192  prjsperref  43193  prjspersym  43194  prjspvs  43197  prjsprellsp  43198  dffltz  43221  irrapx1  43410  pell1234qrne0  43435  pell1234qrreccl  43436  pell1234qrmulcl  43437  pell14qrgt0  43441  pell1234qrdich  43443  pell14qrdich  43451  pell1qrge1  43452  pell1qr1  43453  pell1qrgap  43456  pell14qrgapw  43458  pellqrexplicit  43459  pellqrex  43461  pellfundge  43464  pellfundgt1  43465  setindtr  43606  kelac1  43645  mpaaeu  43732  flcidc  43752  deg1mhm  43782  onexoegt  43826  cantnfub  43903  cantnfresb  43906  succlg  43910  dflim5  43911  onmcl  43913  omabs2  43914  tfsconcatrev  43930  minregex2  44116  radcnvrat  44895  binomcxplemdvbinom  44934  disjiun2  45643  fiiuncl  45650  disjf1o  45774  difmapsn  45793  supminfxr2  46048  icoiccdif  46105  iccdificc  46120  fsumnncl  46153  fsumsupp0  46159  fprod0  46177  climrec  46184  islpcn  46218  lptre2pt  46219  limclner  46230  cnrefiisplem  46408  fprodcncf  46479  fperdvper  46498  dvdivcncf  46506  dvnmul  46522  dvmptfprodlem  46523  dvnprodlem2  46526  stoweidlem25  46604  stoweidlem28  46607  stoweidlem41  46620  stoweidlem44  46623  stoweidlem46  46625  stirlinglem5  46657  dirkercncflem1  46682  dirkercncflem2  46683  fourierdlem24  46710  fourierdlem62  46747  fouriersw  46810  fouriercn  46811  elaa2lem  46812  elaa2  46813  etransclem25  46838  etransclem35  46848  etransclem44  46857  sge0iunmptlemfi  46992  sge0fodjrnlem  46995  iundjiunlem  47038  meadjiunlem  47044  meaiininclem  47065  isomenndlem  47109  hsphoidmvle2  47164  hsphoidmvle  47165  hoidmv1lelem2  47171  hoidmvle  47179  ovnhoilem1  47180  hspdifhsp  47195  hspmbllem2  47206  ovnsubadd2lem  47224  ovolval4lem1  47228  preimagelt  47278  preimalegt  47279  chnsubseq  47461  fsummsndifre  47979  fsummmodsndifre  47981  odz2prm2pw  48177  fmtnoprmfac1lem  48178  fmtnoprmfac2lem1  48180  2pwp1prm  48203  lighneallem2  48220  lighneallem3  48221  lighneallem4  48224  bgoldbtbndlem2  48433  bgoldbtbndlem3  48434  bgoldbtbndlem4  48435  bgoldbtbnd  48436  isubgrvtxuhgr  48491  2zrngnmlid2  48884  mgpsumunsn  48988  mgpsumz  48989  mgpsumn  48990  lindslinindsimp1  49084  lindslinindsimp2  49090  lincresunit1  49104  lincresunit2  49105  lincresunit3lem1  49106  lincresunit3lem2  49107  lincresunit3  49108  lindssnlvec  49113  logcxp0  49162  relogbmulbexp  49188  relogbdivb  49189  dignn0fr  49228  rrxlinesc  49362  eenglngeehlnmlem1  49364  eenglngeehlnmlem2  49365