Theorem eldifi 4077

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3901

This theorem is used by:  difss  4082  eqoreldif  4645  xpdifid  6154  xpdifcnvepel  6155  tz7.7  6377  tfi  7847  peano5  7888  resf1extb  7929  resf1ext2b  7930  xpord2pred  8140  frrlem12  8293  frrlem13  8294  tz7.48-1  8431  tz7.49  8433  dif20el  8491  oaf1o  8549  oeordi  8574  oeord  8575  oecan  8576  oeword  8577  oeworde  8580  oelimcl  8587  oeeulem  8588  oeeui  8589  oaabs2  8636  boxcutc  8947  domdifsn  9057  pssnn  9162  isinf  9234  pwfilem  9287  fsuppco2  9373  fsuppcor  9374  ordtypelem7  9496  unxpwdom2  9560  inf3lem3  9609  cantnfp1lem1  9657  cantnfp1lem3  9659  ttrcltr  9695  elhf3OLD  9894  infxpenc2lem1  10069  dfacacn  10191  isf32lem3  10404  isf34lem4  10426  fin67  10444  isfin7-2  10445  domtriomlem  10491  axdc2lem  10497  axdc3lem4  10502  axdc4lem  10504  ttukeylem7  10564  konigthlem  10624  fpwwe2lem12  10698  fpwwe2  10699  ind0  12299  modfzo0difsn  14054  hashf1lem1  14567  hashle2prv  14590  rlimrege0  15713  rlimrecl  15714  sumrblem  15844  fsumcvg  15845  summolem2a  15848  fsumss  15858  fsumsplit1  15878  fsumless  15930  cvgcmpce  15952  binomlem  15965  incexclem  15972  incexc  15973  isumltss  15984  prodrblem  16063  fprodcvg  16064  prodmolem2a  16068  fprodss  16082  fprodn0f  16125  fprodeq0g  16128  fprodmodd  16131  rpnnen2lem10  16358  rpnnen2lem11  16359  sumeven  16524  sumodd  16525  lcmfunsnlem2  16777  oddprmge3  16838  oddprm  16949  nnoddn2prm  16950  nnoddn2prmb  16952  iserodd  16974  prmreclem2  17056  prmreclem3  17057  prmreclem5  17059  4sqlem19  17102  prmdvdsprmo  17181  prmodvdslcmf  17186  prmlem0  17244  firest  17564  chnccat  18761  chnrev  18762  grpinvnzcl  19182  symgextfv  19593  pmtrf  19630  pmtrdifellem3  19653  sylow2alem2  19793  sylow2a  19794  efgsf  19904  efgsrel  19909  efgs1  19910  efgsfo  19914  gsumzaddlem  20096  gsumzadd  20097  gsumzmhm  20112  gsum2d2lem  20148  dprdfadd  20197  dprdres  20205  subgdmdprd  20211  dmdprdsplitlem  20214  dmdprdsplit2lem  20222  dpjidcl  20235  ablfac1b  20247  pgpfac1lem1  20251  gsummgp0  20508  isirred  20610  irredrmul  20618  ringelnzr  20735  c0rhm  20747  c0rnghm  20748  zrrnghm  20749  zrinitorngc  20855  zrtermorngc  20856  isdomn2  20924  isdomn4  20928  isdrng2  20958  isdrng3lem2  20967  isdrng5  20969  drngmcl  20970  isdrngd  20983  isdrngdOLD  20985  imadrhmcl  21015  cntzsdrg  21020  lcomfsupp  21138  lbspropd  21335  lspsneq  21361  lsppratlem6  21391  lbsextlem2  21398  lbsextlem4  21400  prmidlc2  21591  cmprmidlmcl  21592  cnsubrg  21694  xrs1mnd  21707  xrs10  21708  xrs1cmn  21709  psgnodpm  21855  zrhpsgnodpm  21859  evpmodpmf1o  21863  uvcresum  22060  frlmssuvc1  22061  frlmsslsp  22063  frlmup2  22066  lindfrn  22088  f1lindf  22089  lindfmm  22094  islindf4  22105  lindsenlbs  22118  psrbaglesupp  22191  psrlidm  22230  psrridm  22231  mplsubglem  22267  mpllsslem  22268  mplsubrglem  22272  mplmonmul  22306  mplcoe1  22307  mplcoe5  22310  mplbas2  22312  evlslem3  22350  evlsvvvallem  22361  evlsvvvallem2  22362  evlsvvval  22363  selvvvval  22412  mhpvscacl  22436  psdmul  22448  coe1tmmul2  22556  coe1tmmul  22557  dmatmul  22773  1marepvsma1  22859  mdetdiaglem  22874  mdetrlin  22878  mdetrsca  22879  mdetralt  22884  maducoeval2  22916  madugsum  22919  symgmatr01  22930  gsummatr01lem3  22933  gsummatr01lem4  22934  gsummatr01  22935  smadiadetlem0  22937  smadiadetlem1a  22939  matunitlindflem1  22955  cmpfi  23687  2ndcdisj2  23737  elptr2  23854  ptcnplem  23901  xkopt  23935  kqdisj  24012  fin1aufil  24212  ptcmplem2  24333  ptcmplem3  24334  ptcmplem4  24335  opnsubg  24388  lpbl  24783  blcld  24785  zcld  25094  recld2  25095  reconnlem1  25107  divcn  25150  iundisj  25830  mbfeqalem1  25923  itg1val2  25966  itg1ge0  25968  i1fmullem  25976  i1fadd  25977  itg1addlem4  25981  itg1mulc  25986  itg1lea  25994  itg1le  25995  mbfi1fseqlem4  26000  itg2uba  26025  itg2lea  26026  itg2eqa  26027  itg2splitlem  26030  itg2split  26031  itgeqa  26095  ellimc3  26160  dvaddbr  26219  dvmulbr  26220  dvcobr  26227  dvcjbr  26230  dvrec  26236  dvrecg  26254  dvcnvlem  26257  dvexp3  26259  dveflem  26260  tdeglem4  26339  deg1n0ima  26368  deg1mul3le  26396  ig1peu  26454  ply1termlem  26482  plypf1  26492  plyaddlem1  26493  plymullem1  26494  coeeulem  26504  coeidlem  26517  coeid3  26520  coefv0  26528  coemulhi  26534  coemulc  26535  plyn0mulidp  26565  dvply1  26568  fta1  26592  vieta1lem2  26597  elaa  26602  elqaalem2  26606  preimaaa  26609  aannenlem2  26619  aaliou2  26630  tayl0  26652  dvtaylp  26660  taylthlem1  26663  taylthlem2  26664  pserdvlem2  26718  logbcl  27058  relogbreexp  27066  relogbcxp  27076  cxplogb  27077  dcubic  27137  rlimcnp  27256  jensen  27279  dmgmaddn0  27313  dmlogdmgm  27314  lgamgulmlem2  27320  igamz  27338  gamp1  27348  regamcl  27351  wilthlem2  27359  basellem3  27373  chpub  27510  logexprlim  27515  lgslem1  27587  lgslem4  27590  lgsvalmod  27606  lgsqr  27641  lgsqrmod  27642  lgsqrmodndvds  27643  gausslemma2dlem0b  27647  gausslemma2dlem0c  27648  gausslemma2dlem0i  27654  gausslemma2dlem1a  27655  gausslemma2dlem4  27659  gausslemma2dlem5a  27660  gausslemma2dlem7  27663  gausslemma2d  27664  lgsquad2  27676  m1lgs  27678  2lgsoddprm  27706  2sqreultblem  27738  dchrisum0fno1  27801  rplogsum  27817  ishpg  29170  elntg2  29496  umgrislfupgrlem  29633  usgruspgrb  29697  nbumgrvtx  29860  nbupgrres  29878  isuvtx  29909  cusgrexilem2  29956  cusgrexi  29957  structtocusgr  29960  cusgrres  29962  cusgrfilem2  29970  vtxdginducedm1  30057  cusconngr  30725  2pthfrgr  30818  frgrncvvdeq  30843  frgrwopreglem4  30849  frgrwopreglem5  30855  frgrwopreg  30857  frgrhash2wsp  30866  strlem1  32785  strlem3  32788  strlem4  32789  strlem5  32790  hstrlem3  32796  hstrlem4  32797  iundisjf  33116  suppss3  33248  iundisjfi  33321  suppssnn0  33330  qsdrngi  33952  zringidom  34016  zringfrac  34019  psrmonmul  34115  irngnzply1  34256  qtophaus  34401  elzdif0  34545  measvunilem  34778  sibfof  34906  eulerpartlemb  34934  eulerpartlemf  34936  sseqf  34958  ballotlem5  35066  ballotlemi1  35069  ballotlemii  35070  ballotlemic  35073  ballotlem1c  35074  ballotlemscr  35085  ballotlemro  35089  ballotlemfg  35092  ballotlemfrc  35093  ballotlemfrceq  35095  ballotlemrinv0  35099  signstfvn  35132  signsvfn  35145  bnj923  35333  bnj570  35469  bnj594  35476  fineqvnttrclselem1  35714  fineqvnttrclselem2  35715  fineqvnttrclselem3  35716  fineqvnttrclse  35717  subfacp1lem1  35865  satffunlem2lem1  36090  mrsubcn  36205  mrsubco  36207  circum  36360  dfon2lem6  36472  neibastop1  37069  bj-restn0b  37932  lindsadd  38456  poimirlem24  38482  poimirlem25  38483  dvtan  38508  itg2addnclem2  38510  ftc1cnnc  38530  dvasin  38542  dvreasin  38544  dvreacos  38545  isdrngo2  38812  isdrngo3  38813  divrngidl  38882  isfldidl  38922  pridlc2  38926  pridlc3  38927  blockadjliftmap  39310  prter2  39858  lsateln0  39972  lsatlss  39973  lsmsat  39985  lsatcv0  40008  lsat0cv  40010  lcv1  40018  l1cvpat  40031  dih1dimatlem  42306  dihatexv2  42316  djhcvat42  42392  dihjat1lem  42405  dochsatshp  42428  lcfl6  42477  mapdrvallem2  42622  mapdpglem32  42682  idomnnzgmulnz  43103  aks6d1c5lem3  43107  aks6d1c5lem2  43108  deg1gprod  43110  sticksstones22  43138  unitscyglem4  43168  readvrec2  43340  readvrec  43341  readvcot  43343  evlsbagval  43536  evlselv  43539  evlsmhpvvval  43545  prjspertr  43555  prjsperref  43556  prjspersym  43557  prjspvs  43560  prjsprellsp  43561  dffltz  43584  irrapx1  43773  pell1234qrne0  43798  pell1234qrreccl  43799  pell1234qrmulcl  43800  pell14qrgt0  43804  pell1234qrdich  43806  pell14qrdich  43814  pell1qrge1  43815  pell1qr1  43816  pell1qrgap  43819  pell14qrgapw  43821  pellqrexplicit  43822  pellqrex  43824  pellfundge  43827  pellfundgt1  43828  setindtr  43969  kelac1  44008  mpaaeu  44095  flcidc  44115  deg1mhm  44145  onexoegt  44189  cantnfub  44266  cantnfresb  44269  succlg  44273  dflim5  44274  onmcl  44276  omabs2  44277  tfsconcatrev  44293  minregex2  44479  radcnvrat  45242  binomcxplemdvbinom  45281  disjiun2  45996  fiiuncl  46003  disjf1o  46127  difmapsn  46146  supminfxr2  46401  icoiccdif  46458  iccdificc  46473  fsumnncl  46506  fsumsupp0  46512  fprod0  46530  climrec  46537  islpcn  46571  lptre2pt  46572  limclner  46583  cnrefiisplem  46761  fprodcncf  46832  fperdvper  46851  dvdivcncf  46859  dvnmul  46875  dvmptfprodlem  46876  dvnprodlem2  46879  stoweidlem25  46957  stoweidlem28  46960  stoweidlem41  46973  stoweidlem44  46976  stoweidlem46  46978  stirlinglem5  47010  dirkercncflem1  47035  dirkercncflem2  47036  fourierdlem24  47063  fourierdlem62  47100  fouriersw  47163  fouriercn  47164  elaa2lem  47165  elaa2  47166  etransclem25  47191  etransclem35  47201  etransclem44  47210  sge0iunmptlemfi  47345  sge0fodjrnlem  47348  iundjiunlem  47391  meadjiunlem  47397  meaiininclem  47418  isomenndlem  47462  hsphoidmvle2  47517  hsphoidmvle  47518  hoidmv1lelem2  47524  hoidmvle  47532  ovnhoilem1  47533  hspdifhsp  47548  hspmbllem2  47559  ovnsubadd2lem  47577  ovolval4lem1  47581  preimagelt  47631  preimalegt  47632  chnsubseq  47812  tmachlem-tpopen  47873  fsummsndifre  48372  fsummmodsndifre  48374  odz2prm2pw  48570  fmtnoprmfac1lem  48571  fmtnoprmfac2lem1  48573  2pwp1prm  48596  lighneallem2  48613  lighneallem3  48614  lighneallem4  48617  bgoldbtbndlem2  48826  bgoldbtbndlem3  48827  bgoldbtbndlem4  48828  bgoldbtbnd  48829  isubgrvtxuhgr  48884  2zrngnmlid2  49276  mgpsumunsn  49395  mgpsumz  49396  mgpsumn  49397  lindslinindsimp1  49491  lindslinindsimp2  49497  lincresunit1  49511  lincresunit2  49512  lincresunit3lem1  49513  lincresunit3lem2  49514  lincresunit3  49515  lindssnlvec  49520  logcxp0  49569  relogbmulbexp  49595  relogbdivb  49596  dignn0fr  49635  rrxlinesc  49769  eenglngeehlnmlem1  49771  eenglngeehlnmlem2  49772