Theorem eldifi 4084

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

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

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 3443  df-dif 3905

This theorem is referenced by:  difss  4089  eqoreldif  4643  xpdifid  6127  tz7.7  6344  tfi  7797  peano5  7837  resf1extb  7878  resf1ext2b  7879  xpord2pred  8089  frrlem12  8241  frrlem13  8242  tz7.48-1  8376  tz7.49  8378  dif20el  8434  oaf1o  8492  oeordi  8517  oeord  8518  oecan  8519  oeword  8520  oeworde  8523  oelimcl  8530  oeeulem  8531  oeeui  8532  oaabs2  8579  boxcutc  8883  domdifsn  8992  pssnn  9097  isinf  9169  pwfilem  9222  fsuppco2  9310  fsuppcor  9311  ordtypelem7  9433  unxpwdom2  9497  inf3lem3  9543  cantnfp1lem1  9591  cantnfp1lem3  9593  ttrcltr  9629  infxpenc2lem1  9933  dfacacn  10056  isf32lem3  10269  isf34lem4  10291  fin67  10309  isfin7-2  10310  domtriomlem  10356  axdc2lem  10362  axdc3lem4  10367  axdc4lem  10369  ttukeylem7  10429  konigthlem  10483  fpwwe2lem12  10557  fpwwe2  10558  modfzo0difsn  13870  hashf1lem1  14382  hashle2prv  14405  rlimrege0  15506  rlimrecl  15507  sumrblem  15638  fsumcvg  15639  summolem2a  15642  fsumss  15652  fsumsplit1  15672  fsumless  15723  cvgcmpce  15745  binomlem  15756  incexclem  15763  incexc  15764  isumltss  15775  prodrblem  15856  fprodcvg  15857  prodmolem2a  15861  fprodss  15875  fprodn0f  15918  fprodeq0g  15921  fprodmodd  15924  rpnnen2lem10  16152  rpnnen2lem11  16153  sumeven  16318  sumodd  16319  lcmfunsnlem2  16571  oddprmge3  16631  oddprm  16742  nnoddn2prm  16743  nnoddn2prmb  16745  iserodd  16767  prmreclem2  16849  prmreclem3  16850  prmreclem5  16852  4sqlem19  16895  prmdvdsprmo  16974  prmodvdslcmf  16979  prmlem0  17037  firest  17356  chnccat  18553  chnrev  18554  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  20257  isirred  20359  irredrmul  20367  ringelnzr  20460  c0rhm  20471  c0rnghm  20472  zrrnghm  20473  zrinitorngc  20579  zrtermorngc  20580  isdomn2  20648  isdomn4  20653  isdrng2  20680  drngmcl  20687  isdrngd  20702  isdrngdOLD  20704  imadrhmcl  20734  cntzsdrg  20739  lcomfsupp  20857  lbspropd  21055  lspsneq  21081  lsppratlem6  21111  lbsextlem2  21118  lbsextlem4  21120  cnsubrg  21386  xrs1mnd  21399  xrs10  21400  xrs1cmn  21401  psgnodpm  21547  zrhpsgnodpm  21551  evpmodpmf1o  21555  uvcresum  21752  frlmssuvc1  21753  frlmsslsp  21755  frlmup2  21758  lindfrn  21780  f1lindf  21781  lindfmm  21786  islindf4  21797  psrbaglesupp  21882  psrlidm  21921  psrridm  21922  mplsubglem  21958  mpllsslem  21959  mplsubrglem  21963  mplmonmul  21995  mplcoe1  21996  mplcoe5  21999  mplbas2  22001  evlslem3  22039  evlsvvvallem  22050  evlsvvvallem2  22051  evlsvvval  22052  mhpvscacl  22101  psdmul  22113  coe1tmmul2  22222  coe1tmmul  22223  dmatmul  22445  1marepvsma1  22531  mdetdiaglem  22546  mdetrlin  22550  mdetrsca  22551  mdetralt  22556  maducoeval2  22588  madugsum  22591  symgmatr01  22602  gsummatr01lem3  22605  gsummatr01lem4  22606  gsummatr01  22607  smadiadetlem0  22609  smadiadetlem1a  22611  cmpfi  23356  2ndcdisj2  23405  elptr2  23522  ptcnplem  23569  xkopt  23603  kqdisj  23680  fin1aufil  23880  ptcmplem2  24001  ptcmplem3  24002  ptcmplem4  24003  opnsubg  24056  lpbl  24451  blcld  24453  zcld  24762  recld2  24763  reconnlem1  24775  divcnOLD  24817  divcn  24819  iundisj  25509  mbfeqalem1  25602  itg1val2  25645  itg1ge0  25647  i1fmullem  25655  i1fadd  25656  itg1addlem4  25660  itg1mulc  25665  itg1lea  25673  itg1le  25674  mbfi1fseqlem4  25679  itg2uba  25704  itg2lea  25705  itg2eqa  25706  itg2splitlem  25709  itg2split  25710  itgeqa  25775  ellimc3  25840  dvaddbr  25900  dvmulbr  25901  dvmulbrOLD  25902  dvcobr  25909  dvcobrOLD  25910  dvcjbr  25913  dvrec  25919  dvrecg  25937  dvcnvlem  25940  dvexp3  25942  dveflem  25943  tdeglem4  26025  deg1n0ima  26054  deg1mul3le  26082  ig1peu  26140  ply1termlem  26168  plypf1  26177  plyaddlem1  26178  plymullem1  26179  coeeulem  26189  coeidlem  26202  coeid3  26205  coefv0  26213  coemulhi  26219  coemulc  26220  dvply1  26251  fta1  26276  vieta1lem2  26279  elaa  26284  elqaalem2  26288  aannenlem2  26297  aaliou2  26308  tayl0  26329  dvtaylp  26338  taylthlem1  26341  taylthlem2  26342  taylthlem2OLD  26343  pserdvlem2  26398  logbcl  26737  relogbreexp  26745  relogbcxp  26755  cxplogb  26756  dcubic  26816  rlimcnp  26935  jensen  26959  dmgmaddn0  26993  dmlogdmgm  26994  lgamgulmlem2  27000  igamz  27018  gamp1  27028  regamcl  27031  wilthlem2  27039  basellem3  27053  chpub  27191  logexprlim  27196  lgslem1  27268  lgslem4  27271  lgsvalmod  27287  lgsqr  27322  lgsqrmod  27323  lgsqrmodndvds  27324  gausslemma2dlem0b  27328  gausslemma2dlem0c  27329  gausslemma2dlem0i  27335  gausslemma2dlem1a  27336  gausslemma2dlem4  27340  gausslemma2dlem5a  27341  gausslemma2dlem7  27344  gausslemma2d  27345  lgsquad2  27357  m1lgs  27359  2lgsoddprm  27387  2sqreultblem  27419  dchrisum0fno1  27482  rplogsum  27498  ishpg  28835  elntg2  29062  umgrislfupgrlem  29199  usgruspgrb  29260  nbumgrvtx  29423  nbupgrres  29441  isuvtx  29472  cusgrexilem2  29519  cusgrexi  29520  structtocusgr  29523  cusgrres  29526  cusgrfilem2  29534  vtxdginducedm1  29621  cusconngr  30270  2pthfrgr  30363  frgrncvvdeq  30388  frgrwopreglem4  30394  frgrwopreglem5  30400  frgrwopreg  30402  frgrhash2wsp  30411  strlem1  32329  strlem3  32332  strlem4  32333  strlem5  32334  hstrlem3  32340  hstrlem4  32341  iundisjf  32667  suppss3  32804  iundisjfi  32878  suppssnn0  32887  ind0  32939  qsdrngi  33578  zringidom  33634  zringfrac  33637  irngnzply1  33850  qtophaus  33995  elzdif0  34139  measvunilem  34371  sibfof  34499  eulerpartlemb  34527  eulerpartlemf  34529  sseqf  34551  ballotlem5  34659  ballotlemi1  34662  ballotlemii  34663  ballotlemic  34666  ballotlem1c  34667  ballotlemscr  34678  ballotlemro  34682  ballotlemfg  34685  ballotlemfrc  34686  ballotlemfrceq  34688  ballotlemrinv0  34692  plymulx0  34706  signstfvn  34728  signsvfn  34741  bnj923  34926  bnj570  35063  bnj594  35070  fineqvnttrclselem1  35279  fineqvnttrclselem2  35280  fineqvnttrclselem3  35281  fineqvnttrclse  35282  subfacp1lem1  35375  satffunlem2lem1  35600  mrsubcn  35715  mrsubco  35717  circum  35870  dfon2lem6  35982  neibastop1  36555  bj-restn0b  37298  lindsadd  37816  lindsenlbs  37818  matunitlindflem1  37819  poimirlem24  37847  poimirlem25  37848  dvtan  37873  itg2addnclem2  37875  ftc1cnnc  37895  dvasin  37907  dvreasin  37909  dvreacos  37910  isdrngo2  38161  isdrngo3  38162  divrngidl  38231  isfldidl  38271  pridlc2  38275  pridlc3  38276  blockadjliftmap  38661  prter2  39209  lsateln0  39323  lsatlss  39324  lsmsat  39336  lsatcv0  39359  lsat0cv  39361  lcv1  39369  l1cvpat  39382  dih1dimatlem  41657  dihatexv2  41667  djhcvat42  41743  dihjat1lem  41756  dochsatshp  41779  lcfl6  41828  mapdrvallem2  41973  mapdpglem32  42033  idomnnzgmulnz  42455  aks6d1c5lem3  42459  aks6d1c5lem2  42460  deg1gprod  42462  sticksstones22  42490  unitscyglem4  42520  readvrec2  42683  readvrec  42684  readvcot  42686  evlsbagval  42879  selvvvval  42895  evlselv  42897  evlsmhpvvval  42905  prjspertr  42915  prjsperref  42916  prjspersym  42917  prjspvs  42920  prjsprellsp  42921  dffltz  42944  irrapx1  43137  pell1234qrne0  43162  pell1234qrreccl  43163  pell1234qrmulcl  43164  pell14qrgt0  43168  pell1234qrdich  43170  pell14qrdich  43178  pell1qrge1  43179  pell1qr1  43180  pell1qrgap  43183  pell14qrgapw  43185  pellqrexplicit  43186  pellqrex  43188  pellfundge  43191  pellfundgt1  43192  setindtr  43333  kelac1  43372  mpaaeu  43459  flcidc  43479  deg1mhm  43509  onexoegt  43553  cantnfub  43630  cantnfresb  43633  succlg  43637  dflim5  43638  onmcl  43640  omabs2  43641  tfsconcatrev  43657  minregex2  43843  radcnvrat  44622  binomcxplemdvbinom  44661  disjiun2  45370  fiiuncl  45377  disjf1o  45502  difmapsn  45523  supminfxr2  45780  icoiccdif  45837  iccdificc  45852  fsumnncl  45885  fsumsupp0  45891  fprod0  45909  climrec  45916  islpcn  45950  lptre2pt  45951  limclner  45962  cnrefiisplem  46140  fprodcncf  46211  fperdvper  46230  dvdivcncf  46238  dvnmul  46254  dvmptfprodlem  46255  dvnprodlem2  46258  stoweidlem25  46336  stoweidlem28  46339  stoweidlem41  46352  stoweidlem44  46355  stoweidlem46  46357  stirlinglem5  46389  dirkercncflem1  46414  dirkercncflem2  46415  fourierdlem24  46442  fourierdlem62  46479  fouriersw  46542  fouriercn  46543  elaa2lem  46544  elaa2  46545  etransclem25  46570  etransclem35  46580  etransclem44  46589  sge0iunmptlemfi  46724  sge0fodjrnlem  46727  iundjiunlem  46770  meadjiunlem  46776  meaiininclem  46797  isomenndlem  46841  hsphoidmvle2  46896  hsphoidmvle  46897  hoidmv1lelem2  46903  hoidmvle  46911  ovnhoilem1  46912  hspdifhsp  46927  hspmbllem2  46938  ovnsubadd2lem  46956  ovolval4lem1  46960  preimagelt  47010  preimalegt  47011  chnsubseq  47191  fsummsndifre  47685  fsummmodsndifre  47687  odz2prm2pw  47876  fmtnoprmfac1lem  47877  fmtnoprmfac2lem1  47879  2pwp1prm  47902  lighneallem2  47919  lighneallem3  47920  lighneallem4  47923  bgoldbtbndlem2  48119  bgoldbtbndlem3  48120  bgoldbtbndlem4  48121  bgoldbtbnd  48122  isubgrvtxuhgr  48177  2zrngnmlid2  48570  mgpsumunsn  48674  mgpsumz  48675  mgpsumn  48676  lindslinindsimp1  48770  lindslinindsimp2  48776  lincresunit1  48790  lincresunit2  48791  lincresunit3lem1  48792  lincresunit3lem2  48793  lincresunit3  48794  lindssnlvec  48799  logcxp0  48848  relogbmulbexp  48874  relogbdivb  48875  dignn0fr  48914  rrxlinesc  49048  eenglngeehlnmlem1  49050  eenglngeehlnmlem2  49051