Theorem eldifi 4106

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ∖ cdif 3923

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929

This theorem is referenced by:  difss  4111  eqoreldif  4661  xpdifid  6157  tz7.7  6378  tfi  7846  peano5  7887  resf1extb  7928  resf1ext2b  7929  xpord2pred  8142  frrlem12  8294  frrlem13  8295  wfrlem10OLD  8330  wfrlem15OLD  8335  tz7.48-1  8455  tz7.49  8457  dif20el  8515  oaf1o  8573  oeordi  8597  oeord  8598  oecan  8599  oeword  8600  oeworde  8603  oelimcl  8610  oeeulem  8611  oeeui  8612  oaabs2  8659  boxcutc  8953  domdifsn  9066  pssnn  9180  isinf  9266  isinfOLD  9267  pwfilem  9326  fsuppco2  9413  fsuppcor  9414  ordtypelem7  9536  unxpwdom2  9600  inf3lem3  9642  cantnfp1lem1  9690  cantnfp1lem3  9692  ttrcltr  9728  infxpenc2lem1  10031  dfacacn  10154  isf32lem3  10367  isf34lem4  10389  fin67  10407  isfin7-2  10408  domtriomlem  10454  axdc2lem  10460  axdc3lem4  10465  axdc4lem  10467  ttukeylem7  10527  konigthlem  10580  fpwwe2lem12  10654  fpwwe2  10655  modfzo0difsn  13959  hashf1lem1  14471  hashle2prv  14494  rlimrege0  15593  rlimrecl  15594  sumrblem  15725  fsumcvg  15726  summolem2a  15729  fsumss  15739  fsumsplit1  15759  fsumless  15810  cvgcmpce  15832  binomlem  15843  incexclem  15850  incexc  15851  isumltss  15862  prodrblem  15943  fprodcvg  15944  prodmolem2a  15948  fprodss  15962  fprodn0f  16005  fprodeq0g  16008  fprodmodd  16011  rpnnen2lem10  16239  rpnnen2lem11  16240  sumeven  16404  sumodd  16405  lcmfunsnlem2  16657  oddprmge3  16717  oddprm  16828  nnoddn2prm  16829  nnoddn2prmb  16831  iserodd  16853  prmreclem2  16935  prmreclem3  16936  prmreclem5  16938  4sqlem19  16981  prmdvdsprmo  17060  prmodvdslcmf  17065  prmlem0  17123  firest  17444  grpinvnzcl  18992  symgextfv  19397  pmtrf  19434  pmtrdifellem3  19457  sylow2alem2  19597  sylow2a  19598  efgsf  19708  efgsrel  19713  efgs1  19714  efgsfo  19718  gsumzaddlem  19900  gsumzadd  19901  gsumzmhm  19916  gsum2d2lem  19952  dprdfadd  20001  dprdres  20009  subgdmdprd  20015  dmdprdsplitlem  20018  dmdprdsplit2lem  20026  dpjidcl  20039  ablfac1b  20051  pgpfac1lem1  20055  gsummgp0  20276  isirred  20377  irredrmul  20385  ringelnzr  20481  c0rhm  20492  c0rnghm  20493  zrrnghm  20494  zrinitorngc  20600  zrtermorngc  20601  isdomn2  20669  isdomn4  20674  isdrng2  20701  drngmcl  20708  isdrngd  20723  isdrngdOLD  20725  imadrhmcl  20755  cntzsdrg  20760  lcomfsupp  20857  lbspropd  21055  lspsneq  21081  lsppratlem6  21111  lbsextlem2  21118  lbsextlem4  21120  xrs1mnd  21370  xrs10  21371  xrs1cmn  21372  cnsubrg  21393  psgnodpm  21546  zrhpsgnodpm  21550  evpmodpmf1o  21554  uvcresum  21751  frlmssuvc1  21752  frlmsslsp  21754  frlmup2  21757  lindfrn  21779  f1lindf  21780  lindfmm  21785  islindf4  21796  psrbaglesupp  21880  psrlidm  21920  psrridm  21921  mplsubglem  21957  mpllsslem  21958  mplsubrglem  21962  mplmonmul  21992  mplcoe1  21993  mplcoe5  21996  mplbas2  21998  evlslem3  22036  mhpvscacl  22090  psdmul  22102  coe1tmmul2  22211  coe1tmmul  22212  dmatmul  22433  1marepvsma1  22519  mdetdiaglem  22534  mdetrlin  22538  mdetrsca  22539  mdetralt  22544  maducoeval2  22576  madugsum  22579  symgmatr01  22590  gsummatr01lem3  22593  gsummatr01lem4  22594  gsummatr01  22595  smadiadetlem0  22597  smadiadetlem1a  22599  cmpfi  23344  2ndcdisj2  23393  elptr2  23510  ptcnplem  23557  xkopt  23591  kqdisj  23668  fin1aufil  23868  ptcmplem2  23989  ptcmplem3  23990  ptcmplem4  23991  opnsubg  24044  lpbl  24440  blcld  24442  zcld  24751  recld2  24752  reconnlem1  24764  divcnOLD  24806  divcn  24808  iundisj  25499  mbfeqalem1  25592  itg1val2  25635  itg1ge0  25637  i1fmullem  25645  i1fadd  25646  itg1addlem4  25650  itg1mulc  25655  itg1lea  25663  itg1le  25664  mbfi1fseqlem4  25669  itg2uba  25694  itg2lea  25695  itg2eqa  25696  itg2splitlem  25699  itg2split  25700  itgeqa  25765  ellimc3  25830  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvcobr  25899  dvcobrOLD  25900  dvcjbr  25903  dvrec  25909  dvrecg  25927  dvcnvlem  25930  dvexp3  25932  dveflem  25933  tdeglem4  26015  deg1n0ima  26044  deg1mul3le  26072  ig1peu  26130  ply1termlem  26158  plypf1  26167  plyaddlem1  26168  plymullem1  26169  coeeulem  26179  coeidlem  26192  coeid3  26195  coefv0  26203  coemulhi  26209  coemulc  26210  dvply1  26241  fta1  26266  vieta1lem2  26269  elaa  26274  elqaalem2  26278  aannenlem2  26287  aaliou2  26298  tayl0  26319  dvtaylp  26328  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  pserdvlem2  26388  logbcl  26727  relogbreexp  26735  relogbcxp  26745  cxplogb  26746  dcubic  26806  rlimcnp  26925  jensen  26949  dmgmaddn0  26983  dmlogdmgm  26984  lgamgulmlem2  26990  igamz  27008  gamp1  27018  regamcl  27021  wilthlem2  27029  basellem3  27043  chpub  27181  logexprlim  27186  lgslem1  27258  lgslem4  27261  lgsvalmod  27277  lgsqr  27312  lgsqrmod  27313  lgsqrmodndvds  27314  gausslemma2dlem0b  27318  gausslemma2dlem0c  27319  gausslemma2dlem0i  27325  gausslemma2dlem1a  27326  gausslemma2dlem4  27330  gausslemma2dlem5a  27331  gausslemma2dlem7  27334  gausslemma2d  27335  lgsquad2  27347  m1lgs  27349  2lgsoddprm  27377  2sqreultblem  27409  dchrisum0fno1  27472  rplogsum  27488  ishpg  28684  elntg2  28910  umgrislfupgrlem  29047  usgruspgrb  29108  nbumgrvtx  29271  nbupgrres  29289  isuvtx  29320  cusgrexilem2  29367  cusgrexi  29368  structtocusgr  29371  cusgrres  29374  cusgrfilem2  29382  vtxdginducedm1  29469  cusconngr  30118  2pthfrgr  30211  frgrncvvdeq  30236  frgrwopreglem4  30242  frgrwopreglem5  30248  frgrwopreg  30250  frgrhash2wsp  30259  strlem1  32177  strlem3  32180  strlem4  32181  strlem5  32182  hstrlem3  32188  hstrlem4  32189  iundisjf  32516  suppss3  32647  iundisjfi  32719  suppssnn0  32730  ind0  32781  qsdrngi  33456  zringidom  33512  zringfrac  33515  irngnzply1  33678  qtophaus  33813  elzdif0  33957  measvunilem  34189  sibfof  34318  eulerpartlemb  34346  eulerpartlemf  34348  sseqf  34370  ballotlem5  34478  ballotlemi1  34481  ballotlemii  34482  ballotlemic  34485  ballotlem1c  34486  ballotlemscr  34497  ballotlemro  34501  ballotlemfg  34504  ballotlemfrc  34505  ballotlemfrceq  34507  ballotlemrinv0  34511  plymulx0  34525  signstfvn  34547  signsvfn  34560  bnj923  34745  bnj570  34882  bnj594  34889  subfacp1lem1  35147  satffunlem2lem1  35372  mrsubcn  35487  mrsubco  35489  circum  35642  dfon2lem6  35752  neibastop1  36323  bj-restn0b  37055  lindsadd  37583  lindsenlbs  37585  matunitlindflem1  37586  poimirlem24  37614  poimirlem25  37615  dvtan  37640  itg2addnclem2  37642  ftc1cnnc  37662  dvasin  37674  dvreasin  37676  dvreacos  37677  isdrngo2  37928  isdrngo3  37929  divrngidl  37998  isfldidl  38038  pridlc2  38042  pridlc3  38043  prter2  38845  lsateln0  38959  lsatlss  38960  lsmsat  38972  lsatcv0  38995  lsat0cv  38997  lcv1  39005  l1cvpat  39018  dih1dimatlem  41294  dihatexv2  41304  djhcvat42  41380  dihjat1lem  41393  dochsatshp  41416  lcfl6  41465  mapdrvallem2  41610  mapdpglem32  41670  idomnnzgmulnz  42092  aks6d1c5lem3  42096  aks6d1c5lem2  42097  deg1gprod  42099  sticksstones22  42127  unitscyglem4  42157  readvrec2  42351  readvrec  42352  readvcot  42354  evlsvvvallem  42531  evlsvvvallem2  42532  evlsvvval  42533  evlsbagval  42536  selvvvval  42555  evlselv  42557  evlsmhpvvval  42565  prjspertr  42575  prjsperref  42576  prjspersym  42577  prjspvs  42580  prjsprellsp  42581  dffltz  42604  irrapx1  42798  pell1234qrne0  42823  pell1234qrreccl  42824  pell1234qrmulcl  42825  pell14qrgt0  42829  pell1234qrdich  42831  pell14qrdich  42839  pell1qrge1  42840  pell1qr1  42841  pell1qrgap  42844  pell14qrgapw  42846  pellqrexplicit  42847  pellqrex  42849  pellfundge  42852  pellfundgt1  42853  setindtr  42995  kelac1  43034  mpaaeu  43121  flcidc  43141  deg1mhm  43171  onexoegt  43215  cantnfub  43292  cantnfresb  43295  succlg  43299  dflim5  43300  onmcl  43302  omabs2  43303  tfsconcatrev  43319  minregex2  43506  radcnvrat  44286  binomcxplemdvbinom  44325  disjiun2  45030  fiiuncl  45037  disjf1o  45163  difmapsn  45184  supminfxr2  45444  icoiccdif  45501  iccdificc  45516  fsumnncl  45549  fsumsupp0  45555  fprod0  45573  climrec  45580  islpcn  45616  lptre2pt  45617  limclner  45628  cnrefiisplem  45806  fprodcncf  45877  fperdvper  45896  dvdivcncf  45904  dvnmul  45920  dvmptfprodlem  45921  dvnprodlem2  45924  stoweidlem25  46002  stoweidlem28  46005  stoweidlem41  46018  stoweidlem44  46021  stoweidlem46  46023  stirlinglem5  46055  dirkercncflem1  46080  dirkercncflem2  46081  fourierdlem24  46108  fourierdlem62  46145  fouriersw  46208  fouriercn  46209  elaa2lem  46210  elaa2  46211  etransclem25  46236  etransclem35  46246  etransclem44  46255  sge0iunmptlemfi  46390  sge0fodjrnlem  46393  iundjiunlem  46436  meadjiunlem  46442  meaiininclem  46463  isomenndlem  46507  hsphoidmvle2  46562  hsphoidmvle  46563  hoidmv1lelem2  46569  hoidmvle  46577  ovnhoilem1  46578  hspdifhsp  46593  hspmbllem2  46604  ovnsubadd2lem  46622  ovolval4lem1  46626  preimagelt  46676  preimalegt  46677  fsummsndifre  47334  fsummmodsndifre  47336  odz2prm2pw  47525  fmtnoprmfac1lem  47526  fmtnoprmfac2lem1  47528  2pwp1prm  47551  lighneallem2  47568  lighneallem3  47569  lighneallem4  47572  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  bgoldbtbndlem4  47770  bgoldbtbnd  47771  isubgrvtxuhgr  47825  2zrngnmlid2  48180  mgpsumunsn  48284  mgpsumz  48285  mgpsumn  48286  lindslinindsimp1  48381  lindslinindsimp2  48387  lincresunit1  48401  lincresunit2  48402  lincresunit3lem1  48403  lincresunit3lem2  48404  lincresunit3  48405  lindssnlvec  48410  logcxp0  48463  relogbmulbexp  48489  relogbdivb  48490  dignn0fr  48529  rrxlinesc  48663  eenglngeehlnmlem1  48665  eenglngeehlnmlem2  48666