Theorem eldifi 4072

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893

This theorem is referenced by:  difss  4077  eqoreldif  4630  xpdifid  6124  tz7.7  6341  tfi  7795  peano5  7835  resf1extb  7876  resf1ext2b  7877  xpord2pred  8086  frrlem12  8238  frrlem13  8239  tz7.48-1  8373  tz7.49  8375  dif20el  8431  oaf1o  8489  oeordi  8514  oeord  8515  oecan  8516  oeword  8517  oeworde  8520  oelimcl  8527  oeeulem  8528  oeeui  8529  oaabs2  8576  boxcutc  8880  domdifsn  8989  pssnn  9094  isinf  9166  pwfilem  9219  fsuppco2  9307  fsuppcor  9308  ordtypelem7  9430  unxpwdom2  9494  inf3lem3  9540  cantnfp1lem1  9588  cantnfp1lem3  9590  ttrcltr  9626  infxpenc2lem1  9930  dfacacn  10053  isf32lem3  10266  isf34lem4  10288  fin67  10306  isfin7-2  10307  domtriomlem  10353  axdc2lem  10359  axdc3lem4  10364  axdc4lem  10366  ttukeylem7  10426  konigthlem  10480  fpwwe2lem12  10554  fpwwe2  10555  modfzo0difsn  13867  hashf1lem1  14379  hashle2prv  14402  rlimrege0  15503  rlimrecl  15504  sumrblem  15635  fsumcvg  15636  summolem2a  15639  fsumss  15649  fsumsplit1  15669  fsumless  15720  cvgcmpce  15742  binomlem  15753  incexclem  15760  incexc  15761  isumltss  15772  prodrblem  15853  fprodcvg  15854  prodmolem2a  15858  fprodss  15872  fprodn0f  15915  fprodeq0g  15918  fprodmodd  15921  rpnnen2lem10  16149  rpnnen2lem11  16150  sumeven  16315  sumodd  16316  lcmfunsnlem2  16568  oddprmge3  16628  oddprm  16739  nnoddn2prm  16740  nnoddn2prmb  16742  iserodd  16764  prmreclem2  16846  prmreclem3  16847  prmreclem5  16849  4sqlem19  16892  prmdvdsprmo  16971  prmodvdslcmf  16976  prmlem0  17034  firest  17353  chnccat  18550  chnrev  18551  grpinvnzcl  18945  symgextfv  19351  pmtrf  19388  pmtrdifellem3  19411  sylow2alem2  19551  sylow2a  19552  efgsf  19662  efgsrel  19667  efgs1  19668  efgsfo  19672  gsumzaddlem  19854  gsumzadd  19855  gsumzmhm  19870  gsum2d2lem  19906  dprdfadd  19955  dprdres  19963  subgdmdprd  19969  dmdprdsplitlem  19972  dmdprdsplit2lem  19980  dpjidcl  19993  ablfac1b  20005  pgpfac1lem1  20009  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  21879  psrlidm  21918  psrridm  21919  mplsubglem  21955  mpllsslem  21956  mplsubrglem  21960  mplmonmul  21992  mplcoe1  21993  mplcoe5  21996  mplbas2  21998  evlslem3  22036  evlsvvvallem  22047  evlsvvvallem2  22048  evlsvvval  22049  mhpvscacl  22098  psdmul  22110  coe1tmmul2  22219  coe1tmmul  22220  dmatmul  22440  1marepvsma1  22526  mdetdiaglem  22541  mdetrlin  22545  mdetrsca  22546  mdetralt  22551  maducoeval2  22583  madugsum  22586  symgmatr01  22597  gsummatr01lem3  22600  gsummatr01lem4  22601  gsummatr01  22602  smadiadetlem0  22604  smadiadetlem1a  22606  cmpfi  23351  2ndcdisj2  23400  elptr2  23517  ptcnplem  23564  xkopt  23598  kqdisj  23675  fin1aufil  23875  ptcmplem2  23996  ptcmplem3  23997  ptcmplem4  23998  opnsubg  24051  lpbl  24446  blcld  24448  zcld  24757  recld2  24758  reconnlem1  24770  divcn  24813  iundisj  25493  mbfeqalem1  25586  itg1val2  25629  itg1ge0  25631  i1fmullem  25639  i1fadd  25640  itg1addlem4  25644  itg1mulc  25649  itg1lea  25657  itg1le  25658  mbfi1fseqlem4  25663  itg2uba  25688  itg2lea  25689  itg2eqa  25690  itg2splitlem  25693  itg2split  25694  itgeqa  25759  ellimc3  25824  dvaddbr  25883  dvmulbr  25884  dvcobr  25891  dvcjbr  25894  dvrec  25900  dvrecg  25918  dvcnvlem  25921  dvexp3  25923  dveflem  25924  tdeglem4  26006  deg1n0ima  26035  deg1mul3le  26063  ig1peu  26121  ply1termlem  26149  plypf1  26158  plyaddlem1  26159  plymullem1  26160  coeeulem  26170  coeidlem  26183  coeid3  26186  coefv0  26194  coemulhi  26200  coemulc  26201  dvply1  26231  fta1  26256  vieta1lem2  26259  elaa  26264  elqaalem2  26268  aannenlem2  26277  aaliou2  26288  tayl0  26309  dvtaylp  26318  taylthlem1  26321  taylthlem2  26322  taylthlem2OLD  26323  pserdvlem2  26378  logbcl  26717  relogbreexp  26725  relogbcxp  26735  cxplogb  26736  dcubic  26796  rlimcnp  26915  jensen  26939  dmgmaddn0  26973  dmlogdmgm  26974  lgamgulmlem2  26980  igamz  26998  gamp1  27008  regamcl  27011  wilthlem2  27019  basellem3  27033  chpub  27171  logexprlim  27176  lgslem1  27248  lgslem4  27251  lgsvalmod  27267  lgsqr  27302  lgsqrmod  27303  lgsqrmodndvds  27304  gausslemma2dlem0b  27308  gausslemma2dlem0c  27309  gausslemma2dlem0i  27315  gausslemma2dlem1a  27316  gausslemma2dlem4  27320  gausslemma2dlem5a  27321  gausslemma2dlem7  27324  gausslemma2d  27325  lgsquad2  27337  m1lgs  27339  2lgsoddprm  27367  2sqreultblem  27399  dchrisum0fno1  27462  rplogsum  27478  ishpg  28815  elntg2  29042  umgrislfupgrlem  29179  usgruspgrb  29240  nbumgrvtx  29403  nbupgrres  29421  isuvtx  29452  cusgrexilem2  29499  cusgrexi  29500  structtocusgr  29503  cusgrres  29506  cusgrfilem2  29514  vtxdginducedm1  29601  cusconngr  30250  2pthfrgr  30343  frgrncvvdeq  30368  frgrwopreglem4  30374  frgrwopreglem5  30380  frgrwopreg  30382  frgrhash2wsp  30391  strlem1  32310  strlem3  32313  strlem4  32314  strlem5  32315  hstrlem3  32321  hstrlem4  32322  iundisjf  32648  suppss3  32785  iundisjfi  32859  suppssnn0  32868  ind0  32920  qsdrngi  33560  zringidom  33616  zringfrac  33619  psrmonmul  33699  irngnzply1  33841  qtophaus  33986  elzdif0  34130  measvunilem  34362  sibfof  34490  eulerpartlemb  34518  eulerpartlemf  34520  sseqf  34542  ballotlem5  34650  ballotlemi1  34653  ballotlemii  34654  ballotlemic  34657  ballotlem1c  34658  ballotlemscr  34669  ballotlemro  34673  ballotlemfg  34676  ballotlemfrc  34677  ballotlemfrceq  34679  ballotlemrinv0  34683  plymulx0  34697  signstfvn  34719  signsvfn  34732  bnj923  34917  bnj570  35053  bnj594  35060  fineqvnttrclselem1  35271  fineqvnttrclselem2  35272  fineqvnttrclselem3  35273  fineqvnttrclse  35274  subfacp1lem1  35367  satffunlem2lem1  35592  mrsubcn  35707  mrsubco  35709  circum  35862  dfon2lem6  35974  neibastop1  36547  bj-restn0b  37401  lindsadd  37925  lindsenlbs  37927  matunitlindflem1  37928  poimirlem24  37956  poimirlem25  37957  dvtan  37982  itg2addnclem2  37984  ftc1cnnc  38004  dvasin  38016  dvreasin  38018  dvreacos  38019  isdrngo2  38270  isdrngo3  38271  divrngidl  38340  isfldidl  38380  pridlc2  38384  pridlc3  38385  blockadjliftmap  38770  prter2  39318  lsateln0  39432  lsatlss  39433  lsmsat  39445  lsatcv0  39468  lsat0cv  39470  lcv1  39478  l1cvpat  39491  dih1dimatlem  41766  dihatexv2  41776  djhcvat42  41852  dihjat1lem  41865  dochsatshp  41888  lcfl6  41937  mapdrvallem2  42082  mapdpglem32  42142  idomnnzgmulnz  42564  aks6d1c5lem3  42568  aks6d1c5lem2  42569  deg1gprod  42571  sticksstones22  42599  unitscyglem4  42629  readvrec2  42792  readvrec  42793  readvcot  42795  evlsbagval  43001  selvvvval  43017  evlselv  43019  evlsmhpvvval  43027  prjspertr  43037  prjsperref  43038  prjspersym  43039  prjspvs  43042  prjsprellsp  43043  dffltz  43066  irrapx1  43259  pell1234qrne0  43284  pell1234qrreccl  43285  pell1234qrmulcl  43286  pell14qrgt0  43290  pell1234qrdich  43292  pell14qrdich  43300  pell1qrge1  43301  pell1qr1  43302  pell1qrgap  43305  pell14qrgapw  43307  pellqrexplicit  43308  pellqrex  43310  pellfundge  43313  pellfundgt1  43314  setindtr  43455  kelac1  43494  mpaaeu  43581  flcidc  43601  deg1mhm  43631  onexoegt  43675  cantnfub  43752  cantnfresb  43755  succlg  43759  dflim5  43760  onmcl  43762  omabs2  43763  tfsconcatrev  43779  minregex2  43965  radcnvrat  44744  binomcxplemdvbinom  44783  disjiun2  45492  fiiuncl  45499  disjf1o  45624  difmapsn  45644  supminfxr2  45901  icoiccdif  45958  iccdificc  45973  fsumnncl  46006  fsumsupp0  46012  fprod0  46030  climrec  46037  islpcn  46071  lptre2pt  46072  limclner  46083  cnrefiisplem  46261  fprodcncf  46332  fperdvper  46351  dvdivcncf  46359  dvnmul  46375  dvmptfprodlem  46376  dvnprodlem2  46379  stoweidlem25  46457  stoweidlem28  46460  stoweidlem41  46473  stoweidlem44  46476  stoweidlem46  46478  stirlinglem5  46510  dirkercncflem1  46535  dirkercncflem2  46536  fourierdlem24  46563  fourierdlem62  46600  fouriersw  46663  fouriercn  46664  elaa2lem  46665  elaa2  46666  etransclem25  46691  etransclem35  46701  etransclem44  46710  sge0iunmptlemfi  46845  sge0fodjrnlem  46848  iundjiunlem  46891  meadjiunlem  46897  meaiininclem  46918  isomenndlem  46962  hsphoidmvle2  47017  hsphoidmvle  47018  hoidmv1lelem2  47024  hoidmvle  47032  ovnhoilem1  47033  hspdifhsp  47048  hspmbllem2  47059  ovnsubadd2lem  47077  ovolval4lem1  47081  preimagelt  47131  preimalegt  47132  chnsubseq  47312  fsummsndifre  47806  fsummmodsndifre  47808  odz2prm2pw  47997  fmtnoprmfac1lem  47998  fmtnoprmfac2lem1  48000  2pwp1prm  48023  lighneallem2  48040  lighneallem3  48041  lighneallem4  48044  bgoldbtbndlem2  48240  bgoldbtbndlem3  48241  bgoldbtbndlem4  48242  bgoldbtbnd  48243  isubgrvtxuhgr  48298  2zrngnmlid2  48691  mgpsumunsn  48795  mgpsumz  48796  mgpsumn  48797  lindslinindsimp1  48891  lindslinindsimp2  48897  lincresunit1  48911  lincresunit2  48912  lincresunit3lem1  48913  lincresunit3lem2  48914  lincresunit3  48915  lindssnlvec  48920  logcxp0  48969  relogbmulbexp  48995  relogbdivb  48996  dignn0fr  49035  rrxlinesc  49169  eenglngeehlnmlem1  49171  eenglngeehlnmlem2  49172