Theorem eldifi 4082

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   ∖ cdif 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-dif 3903

This theorem is referenced by:  difss  4087  eqoreldif  4641  xpdifid  6125  tz7.7  6342  tfi  7795  peano5  7835  resf1extb  7876  resf1ext2b  7877  xpord2pred  8087  frrlem12  8239  frrlem13  8240  tz7.48-1  8374  tz7.49  8376  dif20el  8432  oaf1o  8490  oeordi  8515  oeord  8516  oecan  8517  oeword  8518  oeworde  8521  oelimcl  8528  oeeulem  8529  oeeui  8530  oaabs2  8577  boxcutc  8881  domdifsn  8990  pssnn  9095  isinf  9167  pwfilem  9220  fsuppco2  9308  fsuppcor  9309  ordtypelem7  9431  unxpwdom2  9495  inf3lem3  9541  cantnfp1lem1  9589  cantnfp1lem3  9591  ttrcltr  9627  infxpenc2lem1  9931  dfacacn  10054  isf32lem3  10267  isf34lem4  10289  fin67  10307  isfin7-2  10308  domtriomlem  10354  axdc2lem  10360  axdc3lem4  10365  axdc4lem  10367  ttukeylem7  10427  konigthlem  10481  fpwwe2lem12  10555  fpwwe2  10556  modfzo0difsn  13868  hashf1lem1  14380  hashle2prv  14403  rlimrege0  15504  rlimrecl  15505  sumrblem  15636  fsumcvg  15637  summolem2a  15640  fsumss  15650  fsumsplit1  15670  fsumless  15721  cvgcmpce  15743  binomlem  15754  incexclem  15761  incexc  15762  isumltss  15773  prodrblem  15854  fprodcvg  15855  prodmolem2a  15859  fprodss  15873  fprodn0f  15916  fprodeq0g  15919  fprodmodd  15922  rpnnen2lem10  16150  rpnnen2lem11  16151  sumeven  16316  sumodd  16317  lcmfunsnlem2  16569  oddprmge3  16629  oddprm  16740  nnoddn2prm  16741  nnoddn2prmb  16743  iserodd  16765  prmreclem2  16847  prmreclem3  16848  prmreclem5  16850  4sqlem19  16893  prmdvdsprmo  16972  prmodvdslcmf  16977  prmlem0  17035  firest  17354  chnccat  18551  chnrev  18552  grpinvnzcl  18943  symgextfv  19349  pmtrf  19386  pmtrdifellem3  19409  sylow2alem2  19549  sylow2a  19550  efgsf  19660  efgsrel  19665  efgs1  19666  efgsfo  19670  gsumzaddlem  19852  gsumzadd  19853  gsumzmhm  19868  gsum2d2lem  19904  dprdfadd  19953  dprdres  19961  subgdmdprd  19967  dmdprdsplitlem  19970  dmdprdsplit2lem  19978  dpjidcl  19991  ablfac1b  20003  pgpfac1lem1  20007  gsummgp0  20255  isirred  20357  irredrmul  20365  ringelnzr  20458  c0rhm  20469  c0rnghm  20470  zrrnghm  20471  zrinitorngc  20577  zrtermorngc  20578  isdomn2  20646  isdomn4  20651  isdrng2  20678  drngmcl  20685  isdrngd  20700  isdrngdOLD  20702  imadrhmcl  20732  cntzsdrg  20737  lcomfsupp  20855  lbspropd  21053  lspsneq  21079  lsppratlem6  21109  lbsextlem2  21116  lbsextlem4  21118  cnsubrg  21384  xrs1mnd  21397  xrs10  21398  xrs1cmn  21399  psgnodpm  21545  zrhpsgnodpm  21549  evpmodpmf1o  21553  uvcresum  21750  frlmssuvc1  21751  frlmsslsp  21753  frlmup2  21756  lindfrn  21778  f1lindf  21779  lindfmm  21784  islindf4  21795  psrbaglesupp  21880  psrlidm  21919  psrridm  21920  mplsubglem  21956  mpllsslem  21957  mplsubrglem  21961  mplmonmul  21993  mplcoe1  21994  mplcoe5  21997  mplbas2  21999  evlslem3  22037  evlsvvvallem  22048  evlsvvvallem2  22049  evlsvvval  22050  mhpvscacl  22099  psdmul  22111  coe1tmmul2  22220  coe1tmmul  22221  dmatmul  22443  1marepvsma1  22529  mdetdiaglem  22544  mdetrlin  22548  mdetrsca  22549  mdetralt  22554  maducoeval2  22586  madugsum  22589  symgmatr01  22600  gsummatr01lem3  22603  gsummatr01lem4  22604  gsummatr01  22605  smadiadetlem0  22607  smadiadetlem1a  22609  cmpfi  23354  2ndcdisj2  23403  elptr2  23520  ptcnplem  23567  xkopt  23601  kqdisj  23678  fin1aufil  23878  ptcmplem2  23999  ptcmplem3  24000  ptcmplem4  24001  opnsubg  24054  lpbl  24449  blcld  24451  zcld  24760  recld2  24761  reconnlem1  24773  divcnOLD  24815  divcn  24817  iundisj  25507  mbfeqalem1  25600  itg1val2  25643  itg1ge0  25645  i1fmullem  25653  i1fadd  25654  itg1addlem4  25658  itg1mulc  25663  itg1lea  25671  itg1le  25672  mbfi1fseqlem4  25677  itg2uba  25702  itg2lea  25703  itg2eqa  25704  itg2splitlem  25707  itg2split  25708  itgeqa  25773  ellimc3  25838  dvaddbr  25898  dvmulbr  25899  dvmulbrOLD  25900  dvcobr  25907  dvcobrOLD  25908  dvcjbr  25911  dvrec  25917  dvrecg  25935  dvcnvlem  25938  dvexp3  25940  dveflem  25941  tdeglem4  26023  deg1n0ima  26052  deg1mul3le  26080  ig1peu  26138  ply1termlem  26166  plypf1  26175  plyaddlem1  26176  plymullem1  26177  coeeulem  26187  coeidlem  26200  coeid3  26203  coefv0  26211  coemulhi  26217  coemulc  26218  dvply1  26249  fta1  26274  vieta1lem2  26277  elaa  26282  elqaalem2  26286  aannenlem2  26295  aaliou2  26306  tayl0  26327  dvtaylp  26336  taylthlem1  26339  taylthlem2  26340  taylthlem2OLD  26341  pserdvlem2  26396  logbcl  26735  relogbreexp  26743  relogbcxp  26753  cxplogb  26754  dcubic  26814  rlimcnp  26933  jensen  26957  dmgmaddn0  26991  dmlogdmgm  26992  lgamgulmlem2  26998  igamz  27016  gamp1  27026  regamcl  27029  wilthlem2  27037  basellem3  27051  chpub  27189  logexprlim  27194  lgslem1  27266  lgslem4  27269  lgsvalmod  27285  lgsqr  27320  lgsqrmod  27321  lgsqrmodndvds  27322  gausslemma2dlem0b  27326  gausslemma2dlem0c  27327  gausslemma2dlem0i  27333  gausslemma2dlem1a  27334  gausslemma2dlem4  27338  gausslemma2dlem5a  27339  gausslemma2dlem7  27342  gausslemma2d  27343  lgsquad2  27355  m1lgs  27357  2lgsoddprm  27385  2sqreultblem  27417  dchrisum0fno1  27480  rplogsum  27496  ishpg  28812  elntg2  29039  umgrislfupgrlem  29176  usgruspgrb  29237  nbumgrvtx  29400  nbupgrres  29418  isuvtx  29449  cusgrexilem2  29496  cusgrexi  29497  structtocusgr  29500  cusgrres  29503  cusgrfilem2  29511  vtxdginducedm1  29598  cusconngr  30247  2pthfrgr  30340  frgrncvvdeq  30365  frgrwopreglem4  30371  frgrwopreglem5  30377  frgrwopreg  30379  frgrhash2wsp  30388  strlem1  32306  strlem3  32309  strlem4  32310  strlem5  32311  hstrlem3  32317  hstrlem4  32318  iundisjf  32644  suppss3  32781  iundisjfi  32855  suppssnn0  32864  ind0  32916  qsdrngi  33555  zringidom  33611  zringfrac  33614  irngnzply1  33827  qtophaus  33972  elzdif0  34116  measvunilem  34348  sibfof  34476  eulerpartlemb  34504  eulerpartlemf  34506  sseqf  34528  ballotlem5  34636  ballotlemi1  34639  ballotlemii  34640  ballotlemic  34643  ballotlem1c  34644  ballotlemscr  34655  ballotlemro  34659  ballotlemfg  34662  ballotlemfrc  34663  ballotlemfrceq  34665  ballotlemrinv0  34669  plymulx0  34683  signstfvn  34705  signsvfn  34718  bnj923  34903  bnj570  35040  bnj594  35047  fineqvnttrclselem1  35256  fineqvnttrclselem2  35257  fineqvnttrclselem3  35258  fineqvnttrclse  35259  subfacp1lem1  35352  satffunlem2lem1  35577  mrsubcn  35692  mrsubco  35694  circum  35847  dfon2lem6  35959  neibastop1  36532  bj-restn0b  37265  lindsadd  37783  lindsenlbs  37785  matunitlindflem1  37786  poimirlem24  37814  poimirlem25  37815  dvtan  37840  itg2addnclem2  37842  ftc1cnnc  37862  dvasin  37874  dvreasin  37876  dvreacos  37877  isdrngo2  38128  isdrngo3  38129  divrngidl  38198  isfldidl  38238  pridlc2  38242  pridlc3  38243  blockadjliftmap  38628  prter2  39176  lsateln0  39290  lsatlss  39291  lsmsat  39303  lsatcv0  39326  lsat0cv  39328  lcv1  39336  l1cvpat  39349  dih1dimatlem  41624  dihatexv2  41634  djhcvat42  41710  dihjat1lem  41723  dochsatshp  41746  lcfl6  41795  mapdrvallem2  41940  mapdpglem32  42000  idomnnzgmulnz  42422  aks6d1c5lem3  42426  aks6d1c5lem2  42427  deg1gprod  42429  sticksstones22  42457  unitscyglem4  42487  readvrec2  42653  readvrec  42654  readvcot  42656  evlsbagval  42849  selvvvval  42865  evlselv  42867  evlsmhpvvval  42875  prjspertr  42885  prjsperref  42886  prjspersym  42887  prjspvs  42890  prjsprellsp  42891  dffltz  42914  irrapx1  43107  pell1234qrne0  43132  pell1234qrreccl  43133  pell1234qrmulcl  43134  pell14qrgt0  43138  pell1234qrdich  43140  pell14qrdich  43148  pell1qrge1  43149  pell1qr1  43150  pell1qrgap  43153  pell14qrgapw  43155  pellqrexplicit  43156  pellqrex  43158  pellfundge  43161  pellfundgt1  43162  setindtr  43303  kelac1  43342  mpaaeu  43429  flcidc  43449  deg1mhm  43479  onexoegt  43523  cantnfub  43600  cantnfresb  43603  succlg  43607  dflim5  43608  onmcl  43610  omabs2  43611  tfsconcatrev  43627  minregex2  43813  radcnvrat  44592  binomcxplemdvbinom  44631  disjiun2  45340  fiiuncl  45347  disjf1o  45472  difmapsn  45493  supminfxr2  45750  icoiccdif  45807  iccdificc  45822  fsumnncl  45855  fsumsupp0  45861  fprod0  45879  climrec  45886  islpcn  45920  lptre2pt  45921  limclner  45932  cnrefiisplem  46110  fprodcncf  46181  fperdvper  46200  dvdivcncf  46208  dvnmul  46224  dvmptfprodlem  46225  dvnprodlem2  46228  stoweidlem25  46306  stoweidlem28  46309  stoweidlem41  46322  stoweidlem44  46325  stoweidlem46  46327  stirlinglem5  46359  dirkercncflem1  46384  dirkercncflem2  46385  fourierdlem24  46412  fourierdlem62  46449  fouriersw  46512  fouriercn  46513  elaa2lem  46514  elaa2  46515  etransclem25  46540  etransclem35  46550  etransclem44  46559  sge0iunmptlemfi  46694  sge0fodjrnlem  46697  iundjiunlem  46740  meadjiunlem  46746  meaiininclem  46767  isomenndlem  46811  hsphoidmvle2  46866  hsphoidmvle  46867  hoidmv1lelem2  46873  hoidmvle  46881  ovnhoilem1  46882  hspdifhsp  46897  hspmbllem2  46908  ovnsubadd2lem  46926  ovolval4lem1  46930  preimagelt  46980  preimalegt  46981  chnsubseq  47161  fsummsndifre  47655  fsummmodsndifre  47657  odz2prm2pw  47846  fmtnoprmfac1lem  47847  fmtnoprmfac2lem1  47849  2pwp1prm  47872  lighneallem2  47889  lighneallem3  47890  lighneallem4  47893  bgoldbtbndlem2  48089  bgoldbtbndlem3  48090  bgoldbtbndlem4  48091  bgoldbtbnd  48092  isubgrvtxuhgr  48147  2zrngnmlid2  48540  mgpsumunsn  48644  mgpsumz  48645  mgpsumn  48646  lindslinindsimp1  48740  lindslinindsimp2  48746  lincresunit1  48760  lincresunit2  48761  lincresunit3lem1  48762  lincresunit3lem2  48763  lincresunit3  48764  lindssnlvec  48769  logcxp0  48818  relogbmulbexp  48844  relogbdivb  48845  dignn0fr  48884  rrxlinesc  49018  eenglngeehlnmlem1  49020  eenglngeehlnmlem2  49021