Theorem eldifi 4057

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886

This theorem is referenced by:  difss  4062  eqoreldif  4617  xpdifid  6060  tz7.7  6277  tfi  7675  peano5  7714  peano5OLD  7715  frrlem12  8084  frrlem13  8085  wfrlem10OLD  8120  wfrlem15OLD  8125  tz7.48-1  8244  tz7.49  8246  dif20el  8297  oaf1o  8356  oeordi  8380  oeord  8381  oecan  8382  oeword  8383  oeworde  8386  oelimcl  8393  oeeulem  8394  oeeui  8395  oaabs2  8439  boxcutc  8687  domdifsn  8795  pssnn  8913  pwfilem  8922  isinf  8965  pssnnOLD  8969  pwfilemOLD  9043  fsuppco2  9092  fsuppcor  9093  ordtypelem7  9213  unxpwdom2  9277  inf3lem3  9318  cantnfp1lem1  9366  cantnfp1lem3  9368  infxpenc2lem1  9706  dfacacn  9828  isf32lem3  10042  isf34lem4  10064  fin67  10082  isfin7-2  10083  domtriomlem  10129  axdc2lem  10135  axdc3lem4  10140  axdc4lem  10142  ttukeylem7  10202  konigthlem  10255  fpwwe2lem12  10329  fpwwe2  10330  modfzo0difsn  13591  hashf1lem1  14096  hashf1lem1OLD  14097  hashle2prv  14120  rlimrege0  15216  rlimrecl  15217  sumrblem  15351  fsumcvg  15352  summolem2a  15355  fsumss  15365  fsumsplit1  15385  fsumless  15436  cvgcmpce  15458  binomlem  15469  incexclem  15476  incexc  15477  isumltss  15488  prodrblem  15567  fprodcvg  15568  prodmolem2a  15572  fprodss  15586  fprodn0f  15629  fprodeq0g  15632  fprodmodd  15635  rpnnen2lem10  15860  rpnnen2lem11  15861  sumeven  16024  sumodd  16025  lcmfunsnlem2  16273  oddprmge3  16333  oddprm  16439  nnoddn2prm  16440  nnoddn2prmb  16442  iserodd  16464  prmreclem2  16546  prmreclem3  16547  prmreclem5  16549  4sqlem19  16592  prmdvdsprmo  16671  prmodvdslcmf  16676  prmlem0  16735  firest  17060  grpinvnzcl  18562  symgextfv  18941  pmtrf  18978  pmtrdifellem3  19001  sylow2alem2  19138  sylow2a  19139  efgsf  19250  efgsrel  19255  efgs1  19256  efgsfo  19260  gsumzaddlem  19437  gsumzadd  19438  gsumzmhm  19453  gsum2d2lem  19489  dprdfadd  19538  dprdres  19546  subgdmdprd  19552  dmdprdsplitlem  19555  dmdprdsplit2lem  19563  dpjidcl  19576  ablfac1b  19588  pgpfac1lem1  19592  gsummgp0  19762  isirred  19856  irredrmul  19864  isdrng2  19916  isdrngd  19931  cntzsdrg  19985  lcomfsupp  20078  lbspropd  20276  lspsneq  20299  lsppratlem6  20329  lbsextlem2  20336  lbsextlem4  20338  ringelnzr  20450  xrs1mnd  20548  xrs10  20549  xrs1cmn  20550  cnsubrg  20570  psgnodpm  20705  zrhpsgnodpm  20709  evpmodpmf1o  20713  uvcresum  20910  frlmssuvc1  20911  frlmsslsp  20913  frlmup2  20916  lindfrn  20938  f1lindf  20939  lindfmm  20944  islindf4  20955  psrbaglesupp  21037  psrbaglesuppOLD  21038  psrlidm  21082  psrridm  21083  mplsubglem  21115  mpllsslem  21116  mplsubrglem  21120  mplmonmul  21147  mplcoe1  21148  mplcoe5  21151  mplbas2  21153  evlslem3  21200  mhpvscacl  21254  coe1tmmul2  21357  coe1tmmul  21358  dmatmul  21554  1marepvsma1  21640  mdetdiaglem  21655  mdetrlin  21659  mdetrsca  21660  mdetralt  21665  maducoeval2  21697  madugsum  21700  symgmatr01  21711  gsummatr01lem3  21714  gsummatr01lem4  21715  gsummatr01  21716  smadiadetlem0  21718  smadiadetlem1a  21720  cmpfi  22467  2ndcdisj2  22516  elptr2  22633  ptcnplem  22680  xkopt  22714  kqdisj  22791  fin1aufil  22991  ptcmplem2  23112  ptcmplem3  23113  ptcmplem4  23114  opnsubg  23167  lpbl  23565  blcld  23567  zcld  23882  recld2  23883  reconnlem1  23895  divcn  23937  iundisj  24617  mbfeqalem1  24710  itg1val2  24753  itg1ge0  24755  i1fmullem  24763  i1fadd  24764  itg1addlem4  24768  itg1addlem4OLD  24769  itg1mulc  24774  itg1lea  24782  itg1le  24783  mbfi1fseqlem4  24788  itg2uba  24813  itg2lea  24814  itg2eqa  24815  itg2splitlem  24818  itg2split  24819  itgeqa  24883  ellimc3  24948  dvaddbr  25007  dvmulbr  25008  dvcobr  25015  dvcjbr  25018  dvrec  25024  dvrecg  25042  dvcnvlem  25045  dvexp3  25047  dveflem  25048  tdeglem4  25129  tdeglem4OLD  25130  deg1n0ima  25159  deg1mul3le  25186  ig1peu  25241  ply1termlem  25269  plypf1  25278  plyaddlem1  25279  plymullem1  25280  coeeulem  25290  coeidlem  25303  coeid3  25306  coefv0  25314  coemulhi  25320  coemulc  25321  dvply1  25349  fta1  25373  vieta1lem2  25376  elaa  25381  elqaalem2  25385  aannenlem2  25394  aaliou2  25405  tayl0  25426  dvtaylp  25434  taylthlem1  25437  taylthlem2  25438  pserdvlem2  25492  logbcl  25822  relogbreexp  25830  relogbcxp  25840  cxplogb  25841  dcubic  25901  rlimcnp  26020  jensen  26043  dmgmaddn0  26077  dmlogdmgm  26078  lgamgulmlem2  26084  igamz  26102  gamp1  26112  regamcl  26115  wilthlem2  26123  basellem3  26137  chpub  26273  logexprlim  26278  lgslem1  26350  lgslem4  26353  lgsvalmod  26369  lgsqr  26404  lgsqrmod  26405  lgsqrmodndvds  26406  gausslemma2dlem0b  26410  gausslemma2dlem0c  26411  gausslemma2dlem0i  26417  gausslemma2dlem1a  26418  gausslemma2dlem4  26422  gausslemma2dlem5a  26423  gausslemma2dlem7  26426  gausslemma2d  26427  lgsquad2  26439  m1lgs  26441  2lgsoddprm  26469  2sqreultblem  26501  dchrisum0fno1  26564  rplogsum  26580  ishpg  27024  elntg2  27256  umgrislfupgrlem  27395  usgruspgrb  27454  nbumgrvtx  27616  nbupgrres  27634  isuvtx  27665  cusgrexilem2  27712  cusgrexi  27713  structtocusgr  27716  cusgrres  27718  cusgrfilem2  27726  vtxdginducedm1  27813  cusconngr  28456  2pthfrgr  28549  frgrncvvdeq  28574  frgrwopreglem4  28580  frgrwopreglem5  28586  frgrwopreg  28588  frgrhash2wsp  28597  strlem1  30513  strlem3  30516  strlem4  30517  strlem5  30518  hstrlem3  30524  hstrlem4  30525  iundisjf  30829  suppss3  30961  iundisjfi  31019  qtophaus  31688  elzdif0  31830  ind0  31886  measvunilem  32080  sibfof  32207  eulerpartlemb  32235  eulerpartlemf  32237  sseqf  32259  ballotlem5  32366  ballotlemi1  32369  ballotlemii  32370  ballotlemic  32373  ballotlem1c  32374  ballotlemscr  32385  ballotlemro  32389  ballotlemfg  32392  ballotlemfrc  32393  ballotlemfrceq  32395  ballotlemrinv0  32399  plymulx0  32426  signstfvn  32448  signsvfn  32461  bnj923  32648  bnj570  32785  bnj594  32792  subfacp1lem1  33041  satffunlem2lem1  33266  mrsubcn  33381  mrsubco  33383  circum  33532  dfon2lem6  33670  ttrcltr  33702  xpord2pred  33719  neibastop1  34475  bj-restn0b  35189  lindsadd  35697  lindsenlbs  35699  matunitlindflem1  35700  poimirlem24  35728  poimirlem25  35729  dvtan  35754  itg2addnclem2  35756  ftc1cnnc  35776  dvasin  35788  dvreasin  35790  dvreacos  35791  isdrngo2  36043  isdrngo3  36044  divrngidl  36113  isfldidl  36153  pridlc2  36157  pridlc3  36158  prter2  36822  lsateln0  36936  lsatlss  36937  lsmsat  36949  lsatcv0  36972  lsat0cv  36974  lcv1  36982  l1cvpat  36995  dih1dimatlem  39270  dihatexv2  39280  djhcvat42  39356  dihjat1lem  39369  dochsatshp  39392  lcfl6  39441  mapdrvallem2  39586  mapdpglem32  39646  sticksstones22  40052  isdomn4  40100  evlsbagval  40198  prjspertr  40365  prjsperref  40366  prjspersym  40367  prjspvs  40370  prjsprellsp  40371  dffltz  40387  irrapx1  40566  pell1234qrne0  40591  pell1234qrreccl  40592  pell1234qrmulcl  40593  pell14qrgt0  40597  pell1234qrdich  40599  pell14qrdich  40607  pell1qrge1  40608  pell1qr1  40609  pell1qrgap  40612  pell14qrgapw  40614  pellqrexplicit  40615  pellqrex  40617  pellfundge  40620  pellfundgt1  40621  setindtr  40762  kelac1  40804  mpaaeu  40891  flcidc  40915  deg1mhm  40948  radcnvrat  41821  binomcxplemdvbinom  41860  disjiun2  42495  fiiuncl  42502  disjf1o  42618  difmapsn  42641  supminfxr2  42899  icoiccdif  42952  iccdificc  42967  fsumnncl  43003  fsumsupp0  43009  fprod0  43027  climrec  43034  islpcn  43070  lptre2pt  43071  limclner  43082  cnrefiisplem  43260  fprodcncf  43331  fperdvper  43350  dvdivcncf  43358  dvnmul  43374  dvmptfprodlem  43375  dvnprodlem2  43378  stoweidlem25  43456  stoweidlem28  43459  stoweidlem41  43472  stoweidlem44  43475  stoweidlem46  43477  stirlinglem5  43509  dirkercncflem1  43534  dirkercncflem2  43535  fourierdlem24  43562  fourierdlem62  43599  fouriersw  43662  fouriercn  43663  elaa2lem  43664  elaa2  43665  etransclem25  43690  etransclem35  43700  etransclem44  43709  sge0iunmptlemfi  43841  sge0fodjrnlem  43844  iundjiunlem  43887  meadjiunlem  43893  meaiininclem  43914  isomenndlem  43958  hsphoidmvle2  44013  hsphoidmvle  44014  hoidmv1lelem2  44020  hoidmvle  44028  ovnhoilem1  44029  hspdifhsp  44044  hspmbllem2  44055  ovnsubadd2lem  44073  ovolval4lem1  44077  preimagelt  44126  preimalegt  44127  fsummsndifre  44712  fsummmodsndifre  44714  odz2prm2pw  44903  fmtnoprmfac1lem  44904  fmtnoprmfac2lem1  44906  2pwp1prm  44929  lighneallem2  44946  lighneallem3  44947  lighneallem4  44950  bgoldbtbndlem2  45146  bgoldbtbndlem3  45147  bgoldbtbndlem4  45148  bgoldbtbnd  45149  c0rhm  45358  c0rnghm  45359  zrrnghm  45363  2zrngnmlid2  45397  zrinitorngc  45446  zrtermorngc  45447  mgpsumunsn  45585  mgpsumz  45586  mgpsumn  45587  lindslinindsimp1  45686  lindslinindsimp2  45692  lincresunit1  45706  lincresunit2  45707  lincresunit3lem1  45708  lincresunit3lem2  45709  lincresunit3  45710  lindssnlvec  45715  logcxp0  45769  relogbmulbexp  45795  relogbdivb  45796  dignn0fr  45835  rrxlinesc  45969  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972