Theorem eldifi 4081

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145   ∖ cdif 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-dif 3905

This theorem is used by:  difss  4086  eqoreldif  4649  xpdifid  6164  xpdifcnvepel  6165  tz7.7  6387  tfi  7852  peano5  7893  resf1extb  7934  resf1ext2b  7935  xpord2pred  8146  frrlem12  8299  frrlem13  8300  tz7.48-1  8435  tz7.49  8437  dif20el  8495  oaf1o  8553  oeordi  8578  oeord  8579  oecan  8580  oeword  8581  oeworde  8584  oelimcl  8591  oeeulem  8592  oeeui  8593  oaabs2  8640  boxcutc  8951  domdifsn  9061  pssnn  9166  isinf  9238  pwfilem  9290  fsuppco2  9376  fsuppcor  9377  ordtypelem7  9499  unxpwdom2  9563  inf3lem3  9612  cantnfp1lem1  9660  cantnfp1lem3  9662  ttrcltr  9698  infxpenc2lem1  10025  dfacacn  10147  isf32lem3  10360  isf34lem4  10382  fin67  10400  isfin7-2  10401  domtriomlem  10447  axdc2lem  10453  axdc3lem4  10458  axdc4lem  10460  ttukeylem7  10520  konigthlem  10580  fpwwe2lem12  10654  fpwwe2  10655  ind0  12255  modfzo0difsn  14009  hashf1lem1  14522  hashle2prv  14545  rlimrege0  15668  rlimrecl  15669  sumrblem  15799  fsumcvg  15800  summolem2a  15803  fsumss  15813  fsumsplit1  15833  fsumless  15885  cvgcmpce  15907  binomlem  15920  incexclem  15927  incexc  15928  isumltss  15939  prodrblem  16020  fprodcvg  16021  prodmolem2a  16025  fprodss  16039  fprodn0f  16082  fprodeq0g  16085  fprodmodd  16088  rpnnen2lem10  16315  rpnnen2lem11  16316  sumeven  16481  sumodd  16482  lcmfunsnlem2  16734  oddprmge3  16795  oddprm  16906  nnoddn2prm  16907  nnoddn2prmb  16909  iserodd  16931  prmreclem2  17013  prmreclem3  17014  prmreclem5  17016  4sqlem19  17059  prmdvdsprmo  17138  prmodvdslcmf  17143  prmlem0  17201  firest  17521  chnccat  18718  chnrev  18719  grpinvnzcl  19135  symgextfv  19546  pmtrf  19583  pmtrdifellem3  19606  sylow2alem2  19746  sylow2a  19747  efgsf  19857  efgsrel  19862  efgs1  19863  efgsfo  19867  gsumzaddlem  20049  gsumzadd  20050  gsumzmhm  20065  gsum2d2lem  20101  dprdfadd  20150  dprdres  20158  subgdmdprd  20164  dmdprdsplitlem  20167  dmdprdsplit2lem  20175  dpjidcl  20188  ablfac1b  20200  pgpfac1lem1  20204  gsummgp0  20459  isirred  20561  irredrmul  20569  ringelnzr  20685  c0rhm  20697  c0rnghm  20698  zrrnghm  20699  zrinitorngc  20805  zrtermorngc  20806  isdomn2  20874  isdomn4  20878  isdrng2  20907  isdrng3lem2  20916  isdrng5  20918  drngmcl  20919  isdrngd  20932  isdrngdOLD  20934  imadrhmcl  20964  cntzsdrg  20969  lcomfsupp  21087  lbspropd  21284  lspsneq  21310  lsppratlem6  21340  lbsextlem2  21347  lbsextlem4  21349  prmidlc2  21538  cmprmidlmcl  21539  cnsubrg  21641  xrs1mnd  21654  xrs10  21655  xrs1cmn  21656  psgnodpm  21802  zrhpsgnodpm  21806  evpmodpmf1o  21810  uvcresum  22007  frlmssuvc1  22008  frlmsslsp  22010  frlmup2  22013  lindfrn  22035  f1lindf  22036  lindfmm  22041  islindf4  22052  lindsenlbs  22065  psrbaglesupp  22138  psrlidm  22177  psrridm  22178  mplsubglem  22214  mpllsslem  22215  mplsubrglem  22219  mplmonmul  22253  mplcoe1  22254  mplcoe5  22257  mplbas2  22259  evlslem3  22297  evlsvvvallem  22308  evlsvvvallem2  22309  evlsvvval  22310  selvvvval  22359  mhpvscacl  22383  psdmul  22395  coe1tmmul2  22503  coe1tmmul  22504  dmatmul  22720  1marepvsma1  22806  mdetdiaglem  22821  mdetrlin  22825  mdetrsca  22826  mdetralt  22831  maducoeval2  22863  madugsum  22866  symgmatr01  22877  gsummatr01lem3  22880  gsummatr01lem4  22881  gsummatr01  22882  smadiadetlem0  22884  smadiadetlem1a  22886  matunitlindflem1  22902  cmpfi  23634  2ndcdisj2  23684  elptr2  23801  ptcnplem  23848  xkopt  23882  kqdisj  23959  fin1aufil  24159  ptcmplem2  24280  ptcmplem3  24281  ptcmplem4  24282  opnsubg  24335  lpbl  24730  blcld  24732  zcld  25041  recld2  25042  reconnlem1  25054  divcn  25097  iundisj  25777  mbfeqalem1  25870  itg1val2  25913  itg1ge0  25915  i1fmullem  25923  i1fadd  25924  itg1addlem4  25928  itg1mulc  25933  itg1lea  25941  itg1le  25942  mbfi1fseqlem4  25947  itg2uba  25972  itg2lea  25973  itg2eqa  25974  itg2splitlem  25977  itg2split  25978  itgeqa  26043  ellimc3  26108  dvaddbr  26167  dvmulbr  26168  dvcobr  26175  dvcjbr  26178  dvrec  26184  dvrecg  26202  dvcnvlem  26205  dvexp3  26207  dveflem  26208  tdeglem4  26287  deg1n0ima  26316  deg1mul3le  26344  ig1peu  26402  ply1termlem  26430  plypf1  26439  plyaddlem1  26440  plymullem1  26441  coeeulem  26451  coeidlem  26464  coeid3  26467  coefv0  26475  coemulhi  26481  coemulc  26482  plyn0mulidp  26512  dvply1  26515  fta1  26539  vieta1lem2  26542  elaa  26547  elqaalem2  26551  aannenlem2  26562  aaliou2  26573  tayl0  26595  dvtaylp  26603  taylthlem1  26606  taylthlem2  26607  pserdvlem2  26661  logbcl  27002  relogbreexp  27010  relogbcxp  27020  cxplogb  27021  dcubic  27081  rlimcnp  27200  jensen  27223  dmgmaddn0  27257  dmlogdmgm  27258  lgamgulmlem2  27264  igamz  27282  gamp1  27292  regamcl  27295  wilthlem2  27303  basellem3  27317  chpub  27454  logexprlim  27459  lgslem1  27531  lgslem4  27534  lgsvalmod  27550  lgsqr  27585  lgsqrmod  27586  lgsqrmodndvds  27587  gausslemma2dlem0b  27591  gausslemma2dlem0c  27592  gausslemma2dlem0i  27598  gausslemma2dlem1a  27599  gausslemma2dlem4  27603  gausslemma2dlem5a  27604  gausslemma2dlem7  27607  gausslemma2d  27608  lgsquad2  27620  m1lgs  27622  2lgsoddprm  27650  2sqreultblem  27682  dchrisum0fno1  27745  rplogsum  27761  ishpg  29114  elntg2  29428  umgrislfupgrlem  29565  usgruspgrb  29629  nbumgrvtx  29792  nbupgrres  29810  isuvtx  29841  cusgrexilem2  29888  cusgrexi  29889  structtocusgr  29892  cusgrres  29894  cusgrfilem2  29902  vtxdginducedm1  29989  cusconngr  30657  2pthfrgr  30750  frgrncvvdeq  30775  frgrwopreglem4  30781  frgrwopreglem5  30787  frgrwopreg  30789  frgrhash2wsp  30798  strlem1  32717  strlem3  32720  strlem4  32721  strlem5  32722  hstrlem3  32728  hstrlem4  32729  iundisjf  33049  suppss3  33181  iundisjfi  33254  suppssnn0  33263  qsdrngi  33884  zringidom  33948  zringfrac  33951  psrmonmul  34047  irngnzply1  34188  qtophaus  34333  elzdif0  34477  measvunilem  34710  sibfof  34838  eulerpartlemb  34866  eulerpartlemf  34868  sseqf  34890  ballotlem5  34998  ballotlemi1  35001  ballotlemii  35002  ballotlemic  35005  ballotlem1c  35006  ballotlemscr  35017  ballotlemro  35021  ballotlemfg  35024  ballotlemfrc  35025  ballotlemfrceq  35027  ballotlemrinv0  35031  signstfvn  35064  signsvfn  35077  bnj923  35265  bnj570  35401  bnj594  35408  fineqvnttrclselem1  35634  fineqvnttrclselem2  35635  fineqvnttrclselem3  35636  fineqvnttrclse  35637  subfacp1lem1  35745  satffunlem2lem1  35970  mrsubcn  36085  mrsubco  36087  circum  36240  dfon2lem6  36352  neibastop1  36965  bj-restn0b  37828  lindsadd  38354  poimirlem24  38380  poimirlem25  38381  dvtan  38406  itg2addnclem2  38408  ftc1cnnc  38428  dvasin  38440  dvreasin  38442  dvreacos  38443  isdrngo2  38695  isdrngo3  38696  divrngidl  38765  isfldidl  38805  pridlc2  38809  pridlc3  38810  blockadjliftmap  39193  prter2  39741  lsateln0  39855  lsatlss  39856  lsmsat  39868  lsatcv0  39891  lsat0cv  39893  lcv1  39901  l1cvpat  39914  dih1dimatlem  42189  dihatexv2  42199  djhcvat42  42275  dihjat1lem  42288  dochsatshp  42311  lcfl6  42360  mapdrvallem2  42505  mapdpglem32  42565  idomnnzgmulnz  42986  aks6d1c5lem3  42990  aks6d1c5lem2  42991  deg1gprod  42993  sticksstones22  43021  unitscyglem4  43051  readvrec2  43223  readvrec  43224  readvcot  43226  evlsbagval  43419  evlselv  43422  evlsmhpvvval  43428  prjspertr  43438  prjsperref  43439  prjspersym  43440  prjspvs  43443  prjsprellsp  43444  dffltz  43467  irrapx1  43656  pell1234qrne0  43681  pell1234qrreccl  43682  pell1234qrmulcl  43683  pell14qrgt0  43687  pell1234qrdich  43689  pell14qrdich  43697  pell1qrge1  43698  pell1qr1  43699  pell1qrgap  43702  pell14qrgapw  43704  pellqrexplicit  43705  pellqrex  43707  pellfundge  43710  pellfundgt1  43711  setindtr  43852  kelac1  43891  mpaaeu  43978  flcidc  43998  deg1mhm  44028  onexoegt  44072  cantnfub  44149  cantnfresb  44152  succlg  44156  dflim5  44157  onmcl  44159  omabs2  44160  tfsconcatrev  44176  minregex2  44362  radcnvrat  45125  binomcxplemdvbinom  45164  disjiun2  45879  fiiuncl  45886  disjf1o  46010  difmapsn  46029  supminfxr2  46284  icoiccdif  46341  iccdificc  46356  fsumnncl  46389  fsumsupp0  46395  fprod0  46413  climrec  46420  islpcn  46454  lptre2pt  46455  limclner  46466  cnrefiisplem  46644  fprodcncf  46715  fperdvper  46734  dvdivcncf  46742  dvnmul  46758  dvmptfprodlem  46759  dvnprodlem2  46762  stoweidlem25  46840  stoweidlem28  46843  stoweidlem41  46856  stoweidlem44  46859  stoweidlem46  46861  stirlinglem5  46893  dirkercncflem1  46918  dirkercncflem2  46919  fourierdlem24  46946  fourierdlem62  46983  fouriersw  47046  fouriercn  47047  elaa2lem  47048  elaa2  47049  etransclem25  47074  etransclem35  47084  etransclem44  47093  sge0iunmptlemfi  47228  sge0fodjrnlem  47231  iundjiunlem  47274  meadjiunlem  47280  meaiininclem  47301  isomenndlem  47345  hsphoidmvle2  47400  hsphoidmvle  47401  hoidmv1lelem2  47407  hoidmvle  47415  ovnhoilem1  47416  hspdifhsp  47431  hspmbllem2  47442  ovnsubadd2lem  47460  ovolval4lem1  47464  preimagelt  47514  preimalegt  47515  chnsubseq  47695  tmachlem-tpopen  47756  fsummsndifre  48255  fsummmodsndifre  48257  odz2prm2pw  48453  fmtnoprmfac1lem  48454  fmtnoprmfac2lem1  48456  2pwp1prm  48479  lighneallem2  48496  lighneallem3  48497  lighneallem4  48500  bgoldbtbndlem2  48709  bgoldbtbndlem3  48710  bgoldbtbndlem4  48711  bgoldbtbnd  48712  isubgrvtxuhgr  48767  2zrngnmlid2  49159  mgpsumunsn  49278  mgpsumz  49279  mgpsumn  49280  lindslinindsimp1  49374  lindslinindsimp2  49380  lincresunit1  49394  lincresunit2  49395  lincresunit3lem1  49396  lincresunit3lem2  49397  lincresunit3  49398  lindssnlvec  49403  logcxp0  49452  relogbmulbexp  49478  relogbdivb  49479  dignn0fr  49518  rrxlinesc  49652  eenglngeehlnmlem1  49654  eenglngeehlnmlem2  49655