Theorem eldifi 4111

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   ∖ cdif 3928

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 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-dif 3934

This theorem is referenced by:  difss  4116  eqoreldif  4666  xpdifid  6162  tz7.7  6383  tfi  7853  peano5  7894  resf1extb  7935  resf1ext2b  7936  xpord2pred  8149  frrlem12  8301  frrlem13  8302  wfrlem10OLD  8337  wfrlem15OLD  8342  tz7.48-1  8462  tz7.49  8464  dif20el  8522  oaf1o  8580  oeordi  8604  oeord  8605  oecan  8606  oeword  8607  oeworde  8610  oelimcl  8617  oeeulem  8618  oeeui  8619  oaabs2  8666  boxcutc  8960  domdifsn  9073  pssnn  9187  isinf  9273  isinfOLD  9274  pwfilem  9333  fsuppco2  9420  fsuppcor  9421  ordtypelem7  9543  unxpwdom2  9607  inf3lem3  9649  cantnfp1lem1  9697  cantnfp1lem3  9699  ttrcltr  9735  infxpenc2lem1  10038  dfacacn  10161  isf32lem3  10374  isf34lem4  10396  fin67  10414  isfin7-2  10415  domtriomlem  10461  axdc2lem  10467  axdc3lem4  10472  axdc4lem  10474  ttukeylem7  10534  konigthlem  10587  fpwwe2lem12  10661  fpwwe2  10662  modfzo0difsn  13966  hashf1lem1  14478  hashle2prv  14501  rlimrege0  15600  rlimrecl  15601  sumrblem  15732  fsumcvg  15733  summolem2a  15736  fsumss  15746  fsumsplit1  15766  fsumless  15817  cvgcmpce  15839  binomlem  15850  incexclem  15857  incexc  15858  isumltss  15869  prodrblem  15950  fprodcvg  15951  prodmolem2a  15955  fprodss  15969  fprodn0f  16012  fprodeq0g  16015  fprodmodd  16018  rpnnen2lem10  16246  rpnnen2lem11  16247  sumeven  16411  sumodd  16412  lcmfunsnlem2  16664  oddprmge3  16724  oddprm  16835  nnoddn2prm  16836  nnoddn2prmb  16838  iserodd  16860  prmreclem2  16942  prmreclem3  16943  prmreclem5  16945  4sqlem19  16988  prmdvdsprmo  17067  prmodvdslcmf  17072  prmlem0  17130  firest  17451  grpinvnzcl  18999  symgextfv  19404  pmtrf  19441  pmtrdifellem3  19464  sylow2alem2  19604  sylow2a  19605  efgsf  19715  efgsrel  19720  efgs1  19721  efgsfo  19725  gsumzaddlem  19907  gsumzadd  19908  gsumzmhm  19923  gsum2d2lem  19959  dprdfadd  20008  dprdres  20016  subgdmdprd  20022  dmdprdsplitlem  20025  dmdprdsplit2lem  20033  dpjidcl  20046  ablfac1b  20058  pgpfac1lem1  20062  gsummgp0  20283  isirred  20384  irredrmul  20392  ringelnzr  20488  c0rhm  20499  c0rnghm  20500  zrrnghm  20501  zrinitorngc  20607  zrtermorngc  20608  isdomn2  20676  isdomn4  20681  isdrng2  20708  drngmcl  20715  isdrngd  20730  isdrngdOLD  20732  imadrhmcl  20762  cntzsdrg  20767  lcomfsupp  20864  lbspropd  21062  lspsneq  21088  lsppratlem6  21118  lbsextlem2  21125  lbsextlem4  21127  xrs1mnd  21377  xrs10  21378  xrs1cmn  21379  cnsubrg  21400  psgnodpm  21553  zrhpsgnodpm  21557  evpmodpmf1o  21561  uvcresum  21758  frlmssuvc1  21759  frlmsslsp  21761  frlmup2  21764  lindfrn  21786  f1lindf  21787  lindfmm  21792  islindf4  21803  psrbaglesupp  21887  psrlidm  21927  psrridm  21928  mplsubglem  21964  mpllsslem  21965  mplsubrglem  21969  mplmonmul  21999  mplcoe1  22000  mplcoe5  22003  mplbas2  22005  evlslem3  22043  mhpvscacl  22097  psdmul  22109  coe1tmmul2  22218  coe1tmmul  22219  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  24447  blcld  24449  zcld  24758  recld2  24759  reconnlem1  24771  divcnOLD  24813  divcn  24815  iundisj  25506  mbfeqalem1  25599  itg1val2  25642  itg1ge0  25644  i1fmullem  25652  i1fadd  25653  itg1addlem4  25657  itg1mulc  25662  itg1lea  25670  itg1le  25671  mbfi1fseqlem4  25676  itg2uba  25701  itg2lea  25702  itg2eqa  25703  itg2splitlem  25706  itg2split  25707  itgeqa  25772  ellimc3  25837  dvaddbr  25897  dvmulbr  25898  dvmulbrOLD  25899  dvcobr  25906  dvcobrOLD  25907  dvcjbr  25910  dvrec  25916  dvrecg  25934  dvcnvlem  25937  dvexp3  25939  dveflem  25940  tdeglem4  26022  deg1n0ima  26051  deg1mul3le  26079  ig1peu  26137  ply1termlem  26165  plypf1  26174  plyaddlem1  26175  plymullem1  26176  coeeulem  26186  coeidlem  26199  coeid3  26202  coefv0  26210  coemulhi  26216  coemulc  26217  dvply1  26248  fta1  26273  vieta1lem2  26276  elaa  26281  elqaalem2  26285  aannenlem2  26294  aaliou2  26305  tayl0  26326  dvtaylp  26335  taylthlem1  26338  taylthlem2  26339  taylthlem2OLD  26340  pserdvlem2  26395  logbcl  26734  relogbreexp  26742  relogbcxp  26752  cxplogb  26753  dcubic  26813  rlimcnp  26932  jensen  26956  dmgmaddn0  26990  dmlogdmgm  26991  lgamgulmlem2  26997  igamz  27015  gamp1  27025  regamcl  27028  wilthlem2  27036  basellem3  27050  chpub  27188  logexprlim  27193  lgslem1  27265  lgslem4  27268  lgsvalmod  27284  lgsqr  27319  lgsqrmod  27320  lgsqrmodndvds  27321  gausslemma2dlem0b  27325  gausslemma2dlem0c  27326  gausslemma2dlem0i  27332  gausslemma2dlem1a  27333  gausslemma2dlem4  27337  gausslemma2dlem5a  27338  gausslemma2dlem7  27341  gausslemma2d  27342  lgsquad2  27354  m1lgs  27356  2lgsoddprm  27384  2sqreultblem  27416  dchrisum0fno1  27479  rplogsum  27495  ishpg  28743  elntg2  28969  umgrislfupgrlem  29106  usgruspgrb  29167  nbumgrvtx  29330  nbupgrres  29348  isuvtx  29379  cusgrexilem2  29426  cusgrexi  29427  structtocusgr  29430  cusgrres  29433  cusgrfilem2  29441  vtxdginducedm1  29528  cusconngr  30177  2pthfrgr  30270  frgrncvvdeq  30295  frgrwopreglem4  30301  frgrwopreglem5  30307  frgrwopreg  30309  frgrhash2wsp  30318  strlem1  32236  strlem3  32239  strlem4  32240  strlem5  32241  hstrlem3  32247  hstrlem4  32248  iundisjf  32575  suppss3  32706  iundisjfi  32778  suppssnn0  32789  ind0  32840  qsdrngi  33515  zringidom  33571  zringfrac  33574  irngnzply1  33737  qtophaus  33872  elzdif0  34016  measvunilem  34248  sibfof  34377  eulerpartlemb  34405  eulerpartlemf  34407  sseqf  34429  ballotlem5  34537  ballotlemi1  34540  ballotlemii  34541  ballotlemic  34544  ballotlem1c  34545  ballotlemscr  34556  ballotlemro  34560  ballotlemfg  34563  ballotlemfrc  34564  ballotlemfrceq  34566  ballotlemrinv0  34570  plymulx0  34584  signstfvn  34606  signsvfn  34619  bnj923  34804  bnj570  34941  bnj594  34948  subfacp1lem1  35206  satffunlem2lem1  35431  mrsubcn  35546  mrsubco  35548  circum  35701  dfon2lem6  35811  neibastop1  36382  bj-restn0b  37114  lindsadd  37642  lindsenlbs  37644  matunitlindflem1  37645  poimirlem24  37673  poimirlem25  37674  dvtan  37699  itg2addnclem2  37701  ftc1cnnc  37721  dvasin  37733  dvreasin  37735  dvreacos  37736  isdrngo2  37987  isdrngo3  37988  divrngidl  38057  isfldidl  38097  pridlc2  38101  pridlc3  38102  prter2  38904  lsateln0  39018  lsatlss  39019  lsmsat  39031  lsatcv0  39054  lsat0cv  39056  lcv1  39064  l1cvpat  39077  dih1dimatlem  41353  dihatexv2  41363  djhcvat42  41439  dihjat1lem  41452  dochsatshp  41475  lcfl6  41524  mapdrvallem2  41669  mapdpglem32  41729  idomnnzgmulnz  42151  aks6d1c5lem3  42155  aks6d1c5lem2  42156  deg1gprod  42158  sticksstones22  42186  unitscyglem4  42216  readvrec2  42379  readvrec  42380  readvcot  42382  evlsvvvallem  42559  evlsvvvallem2  42560  evlsvvval  42561  evlsbagval  42564  selvvvval  42583  evlselv  42585  evlsmhpvvval  42593  prjspertr  42603  prjsperref  42604  prjspersym  42605  prjspvs  42608  prjsprellsp  42609  dffltz  42632  irrapx1  42826  pell1234qrne0  42851  pell1234qrreccl  42852  pell1234qrmulcl  42853  pell14qrgt0  42857  pell1234qrdich  42859  pell14qrdich  42867  pell1qrge1  42868  pell1qr1  42869  pell1qrgap  42872  pell14qrgapw  42874  pellqrexplicit  42875  pellqrex  42877  pellfundge  42880  pellfundgt1  42881  setindtr  43023  kelac1  43062  mpaaeu  43149  flcidc  43169  deg1mhm  43199  onexoegt  43243  cantnfub  43320  cantnfresb  43323  succlg  43327  dflim5  43328  onmcl  43330  omabs2  43331  tfsconcatrev  43347  minregex2  43534  radcnvrat  44313  binomcxplemdvbinom  44352  disjiun2  45062  fiiuncl  45069  disjf1o  45195  difmapsn  45216  supminfxr2  45476  icoiccdif  45533  iccdificc  45548  fsumnncl  45581  fsumsupp0  45587  fprod0  45605  climrec  45612  islpcn  45648  lptre2pt  45649  limclner  45660  cnrefiisplem  45838  fprodcncf  45909  fperdvper  45928  dvdivcncf  45936  dvnmul  45952  dvmptfprodlem  45953  dvnprodlem2  45956  stoweidlem25  46034  stoweidlem28  46037  stoweidlem41  46050  stoweidlem44  46053  stoweidlem46  46055  stirlinglem5  46087  dirkercncflem1  46112  dirkercncflem2  46113  fourierdlem24  46140  fourierdlem62  46177  fouriersw  46240  fouriercn  46241  elaa2lem  46242  elaa2  46243  etransclem25  46268  etransclem35  46278  etransclem44  46287  sge0iunmptlemfi  46422  sge0fodjrnlem  46425  iundjiunlem  46468  meadjiunlem  46474  meaiininclem  46495  isomenndlem  46539  hsphoidmvle2  46594  hsphoidmvle  46595  hoidmv1lelem2  46601  hoidmvle  46609  ovnhoilem1  46610  hspdifhsp  46625  hspmbllem2  46636  ovnsubadd2lem  46654  ovolval4lem1  46658  preimagelt  46708  preimalegt  46709  fsummsndifre  47366  fsummmodsndifre  47368  odz2prm2pw  47557  fmtnoprmfac1lem  47558  fmtnoprmfac2lem1  47560  2pwp1prm  47583  lighneallem2  47600  lighneallem3  47601  lighneallem4  47604  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  bgoldbtbndlem4  47802  bgoldbtbnd  47803  isubgrvtxuhgr  47857  2zrngnmlid2  48212  mgpsumunsn  48316  mgpsumz  48317  mgpsumn  48318  lindslinindsimp1  48413  lindslinindsimp2  48419  lincresunit1  48433  lincresunit2  48434  lincresunit3lem1  48435  lincresunit3lem2  48436  lincresunit3  48437  lindssnlvec  48442  logcxp0  48495  relogbmulbexp  48521  relogbdivb  48522  dignn0fr  48561  rrxlinesc  48695  eenglngeehlnmlem1  48697  eenglngeehlnmlem2  48698