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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906

This theorem is referenced by:  difss  4087  eqoreldif  4637  xpdifid  6117  tz7.7  6333  tfi  7786  peano5  7826  resf1extb  7867  resf1ext2b  7868  xpord2pred  8078  frrlem12  8230  frrlem13  8231  tz7.48-1  8365  tz7.49  8367  dif20el  8423  oaf1o  8481  oeordi  8505  oeord  8506  oecan  8507  oeword  8508  oeworde  8511  oelimcl  8518  oeeulem  8519  oeeui  8520  oaabs2  8567  boxcutc  8868  domdifsn  8977  pssnn  9082  isinf  9154  pwfilem  9207  fsuppco2  9293  fsuppcor  9294  ordtypelem7  9416  unxpwdom2  9480  inf3lem3  9526  cantnfp1lem1  9574  cantnfp1lem3  9576  ttrcltr  9612  infxpenc2lem1  9913  dfacacn  10036  isf32lem3  10249  isf34lem4  10271  fin67  10289  isfin7-2  10290  domtriomlem  10336  axdc2lem  10342  axdc3lem4  10347  axdc4lem  10349  ttukeylem7  10409  konigthlem  10462  fpwwe2lem12  10536  fpwwe2  10537  modfzo0difsn  13850  hashf1lem1  14362  hashle2prv  14385  rlimrege0  15486  rlimrecl  15487  sumrblem  15618  fsumcvg  15619  summolem2a  15622  fsumss  15632  fsumsplit1  15652  fsumless  15703  cvgcmpce  15725  binomlem  15736  incexclem  15743  incexc  15744  isumltss  15755  prodrblem  15836  fprodcvg  15837  prodmolem2a  15841  fprodss  15855  fprodn0f  15898  fprodeq0g  15901  fprodmodd  15904  rpnnen2lem10  16132  rpnnen2lem11  16133  sumeven  16298  sumodd  16299  lcmfunsnlem2  16551  oddprmge3  16611  oddprm  16722  nnoddn2prm  16723  nnoddn2prmb  16725  iserodd  16747  prmreclem2  16829  prmreclem3  16830  prmreclem5  16832  4sqlem19  16875  prmdvdsprmo  16954  prmodvdslcmf  16959  prmlem0  17017  firest  17336  grpinvnzcl  18890  symgextfv  19297  pmtrf  19334  pmtrdifellem3  19357  sylow2alem2  19497  sylow2a  19498  efgsf  19608  efgsrel  19613  efgs1  19614  efgsfo  19618  gsumzaddlem  19800  gsumzadd  19801  gsumzmhm  19816  gsum2d2lem  19852  dprdfadd  19901  dprdres  19909  subgdmdprd  19915  dmdprdsplitlem  19918  dmdprdsplit2lem  19926  dpjidcl  19939  ablfac1b  19951  pgpfac1lem1  19955  gsummgp0  20203  isirred  20304  irredrmul  20312  ringelnzr  20408  c0rhm  20419  c0rnghm  20420  zrrnghm  20421  zrinitorngc  20527  zrtermorngc  20528  isdomn2  20596  isdomn4  20601  isdrng2  20628  drngmcl  20635  isdrngd  20650  isdrngdOLD  20652  imadrhmcl  20682  cntzsdrg  20687  lcomfsupp  20805  lbspropd  21003  lspsneq  21029  lsppratlem6  21059  lbsextlem2  21066  lbsextlem4  21068  cnsubrg  21334  xrs1mnd  21347  xrs10  21348  xrs1cmn  21349  psgnodpm  21495  zrhpsgnodpm  21499  evpmodpmf1o  21503  uvcresum  21700  frlmssuvc1  21701  frlmsslsp  21703  frlmup2  21706  lindfrn  21728  f1lindf  21729  lindfmm  21734  islindf4  21745  psrbaglesupp  21829  psrlidm  21869  psrridm  21870  mplsubglem  21906  mpllsslem  21907  mplsubrglem  21911  mplmonmul  21941  mplcoe1  21942  mplcoe5  21945  mplbas2  21947  evlslem3  21985  mhpvscacl  22039  psdmul  22051  coe1tmmul2  22160  coe1tmmul  22161  dmatmul  22382  1marepvsma1  22468  mdetdiaglem  22483  mdetrlin  22487  mdetrsca  22488  mdetralt  22493  maducoeval2  22525  madugsum  22528  symgmatr01  22539  gsummatr01lem3  22542  gsummatr01lem4  22543  gsummatr01  22544  smadiadetlem0  22546  smadiadetlem1a  22548  cmpfi  23293  2ndcdisj2  23342  elptr2  23459  ptcnplem  23506  xkopt  23540  kqdisj  23617  fin1aufil  23817  ptcmplem2  23938  ptcmplem3  23939  ptcmplem4  23940  opnsubg  23993  lpbl  24389  blcld  24391  zcld  24700  recld2  24701  reconnlem1  24713  divcnOLD  24755  divcn  24757  iundisj  25447  mbfeqalem1  25540  itg1val2  25583  itg1ge0  25585  i1fmullem  25593  i1fadd  25594  itg1addlem4  25598  itg1mulc  25603  itg1lea  25611  itg1le  25612  mbfi1fseqlem4  25617  itg2uba  25642  itg2lea  25643  itg2eqa  25644  itg2splitlem  25647  itg2split  25648  itgeqa  25713  ellimc3  25778  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  dvcobr  25847  dvcobrOLD  25848  dvcjbr  25851  dvrec  25857  dvrecg  25875  dvcnvlem  25878  dvexp3  25880  dveflem  25881  tdeglem4  25963  deg1n0ima  25992  deg1mul3le  26020  ig1peu  26078  ply1termlem  26106  plypf1  26115  plyaddlem1  26116  plymullem1  26117  coeeulem  26127  coeidlem  26140  coeid3  26143  coefv0  26151  coemulhi  26157  coemulc  26158  dvply1  26189  fta1  26214  vieta1lem2  26217  elaa  26222  elqaalem2  26226  aannenlem2  26235  aaliou2  26246  tayl0  26267  dvtaylp  26276  taylthlem1  26279  taylthlem2  26280  taylthlem2OLD  26281  pserdvlem2  26336  logbcl  26675  relogbreexp  26683  relogbcxp  26693  cxplogb  26694  dcubic  26754  rlimcnp  26873  jensen  26897  dmgmaddn0  26931  dmlogdmgm  26932  lgamgulmlem2  26938  igamz  26956  gamp1  26966  regamcl  26969  wilthlem2  26977  basellem3  26991  chpub  27129  logexprlim  27134  lgslem1  27206  lgslem4  27209  lgsvalmod  27225  lgsqr  27260  lgsqrmod  27261  lgsqrmodndvds  27262  gausslemma2dlem0b  27266  gausslemma2dlem0c  27267  gausslemma2dlem0i  27273  gausslemma2dlem1a  27274  gausslemma2dlem4  27278  gausslemma2dlem5a  27279  gausslemma2dlem7  27282  gausslemma2d  27283  lgsquad2  27295  m1lgs  27297  2lgsoddprm  27325  2sqreultblem  27357  dchrisum0fno1  27420  rplogsum  27436  ishpg  28708  elntg2  28934  umgrislfupgrlem  29071  usgruspgrb  29132  nbumgrvtx  29295  nbupgrres  29313  isuvtx  29344  cusgrexilem2  29391  cusgrexi  29392  structtocusgr  29395  cusgrres  29398  cusgrfilem2  29406  vtxdginducedm1  29493  cusconngr  30139  2pthfrgr  30232  frgrncvvdeq  30257  frgrwopreglem4  30263  frgrwopreglem5  30269  frgrwopreg  30271  frgrhash2wsp  30280  strlem1  32198  strlem3  32201  strlem4  32202  strlem5  32203  hstrlem3  32209  hstrlem4  32210  iundisjf  32538  suppss3  32675  iundisjfi  32748  suppssnn0  32759  ind0  32810  qsdrngi  33441  zringidom  33497  zringfrac  33500  irngnzply1  33674  qtophaus  33819  elzdif0  33963  measvunilem  34195  sibfof  34324  eulerpartlemb  34352  eulerpartlemf  34354  sseqf  34376  ballotlem5  34484  ballotlemi1  34487  ballotlemii  34488  ballotlemic  34491  ballotlem1c  34492  ballotlemscr  34503  ballotlemro  34507  ballotlemfg  34510  ballotlemfrc  34511  ballotlemfrceq  34513  ballotlemrinv0  34517  plymulx0  34531  signstfvn  34553  signsvfn  34566  bnj923  34751  bnj570  34888  bnj594  34895  fineqvnttrclselem1  35090  fineqvnttrclselem2  35091  fineqvnttrclselem3  35092  fineqvnttrclse  35093  subfacp1lem1  35172  satffunlem2lem1  35397  mrsubcn  35512  mrsubco  35514  circum  35667  dfon2lem6  35782  neibastop1  36353  bj-restn0b  37085  lindsadd  37613  lindsenlbs  37615  matunitlindflem1  37616  poimirlem24  37644  poimirlem25  37645  dvtan  37670  itg2addnclem2  37672  ftc1cnnc  37692  dvasin  37704  dvreasin  37706  dvreacos  37707  isdrngo2  37958  isdrngo3  37959  divrngidl  38028  isfldidl  38068  pridlc2  38072  pridlc3  38073  prter2  38880  lsateln0  38994  lsatlss  38995  lsmsat  39007  lsatcv0  39030  lsat0cv  39032  lcv1  39040  l1cvpat  39053  dih1dimatlem  41328  dihatexv2  41338  djhcvat42  41414  dihjat1lem  41427  dochsatshp  41450  lcfl6  41499  mapdrvallem2  41644  mapdpglem32  41704  idomnnzgmulnz  42126  aks6d1c5lem3  42130  aks6d1c5lem2  42131  deg1gprod  42133  sticksstones22  42161  unitscyglem4  42191  readvrec2  42354  readvrec  42355  readvcot  42357  evlsvvvallem  42554  evlsvvvallem2  42555  evlsvvval  42556  evlsbagval  42559  selvvvval  42578  evlselv  42580  evlsmhpvvval  42588  prjspertr  42598  prjsperref  42599  prjspersym  42600  prjspvs  42603  prjsprellsp  42604  dffltz  42627  irrapx1  42821  pell1234qrne0  42846  pell1234qrreccl  42847  pell1234qrmulcl  42848  pell14qrgt0  42852  pell1234qrdich  42854  pell14qrdich  42862  pell1qrge1  42863  pell1qr1  42864  pell1qrgap  42867  pell14qrgapw  42869  pellqrexplicit  42870  pellqrex  42872  pellfundge  42875  pellfundgt1  42876  setindtr  43017  kelac1  43056  mpaaeu  43143  flcidc  43163  deg1mhm  43193  onexoegt  43237  cantnfub  43314  cantnfresb  43317  succlg  43321  dflim5  43322  onmcl  43324  omabs2  43325  tfsconcatrev  43341  minregex2  43528  radcnvrat  44307  binomcxplemdvbinom  44346  disjiun2  45056  fiiuncl  45063  disjf1o  45189  difmapsn  45210  supminfxr2  45468  icoiccdif  45525  iccdificc  45540  fsumnncl  45573  fsumsupp0  45579  fprod0  45597  climrec  45604  islpcn  45640  lptre2pt  45641  limclner  45652  cnrefiisplem  45830  fprodcncf  45901  fperdvper  45920  dvdivcncf  45928  dvnmul  45944  dvmptfprodlem  45945  dvnprodlem2  45948  stoweidlem25  46026  stoweidlem28  46029  stoweidlem41  46042  stoweidlem44  46045  stoweidlem46  46047  stirlinglem5  46079  dirkercncflem1  46104  dirkercncflem2  46105  fourierdlem24  46132  fourierdlem62  46169  fouriersw  46232  fouriercn  46233  elaa2lem  46234  elaa2  46235  etransclem25  46260  etransclem35  46270  etransclem44  46279  sge0iunmptlemfi  46414  sge0fodjrnlem  46417  iundjiunlem  46460  meadjiunlem  46466  meaiininclem  46487  isomenndlem  46531  hsphoidmvle2  46586  hsphoidmvle  46587  hoidmv1lelem2  46593  hoidmvle  46601  ovnhoilem1  46602  hspdifhsp  46617  hspmbllem2  46628  ovnsubadd2lem  46646  ovolval4lem1  46650  preimagelt  46700  preimalegt  46701  fsummsndifre  47376  fsummmodsndifre  47378  odz2prm2pw  47567  fmtnoprmfac1lem  47568  fmtnoprmfac2lem1  47570  2pwp1prm  47593  lighneallem2  47610  lighneallem3  47611  lighneallem4  47614  bgoldbtbndlem2  47810  bgoldbtbndlem3  47811  bgoldbtbndlem4  47812  bgoldbtbnd  47813  isubgrvtxuhgr  47868  2zrngnmlid2  48261  mgpsumunsn  48365  mgpsumz  48366  mgpsumn  48367  lindslinindsimp1  48462  lindslinindsimp2  48468  lincresunit1  48482  lincresunit2  48483  lincresunit3lem1  48484  lincresunit3lem2  48485  lincresunit3  48486  lindssnlvec  48491  logcxp0  48540  relogbmulbexp  48566  relogbdivb  48567  dignn0fr  48606  rrxlinesc  48740  eenglngeehlnmlem1  48742  eenglngeehlnmlem2  48743