Theorem eldifi 4078

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111   ∖ cdif 3894

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900

This theorem is referenced by:  difss  4083  eqoreldif  4635  xpdifid  6115  tz7.7  6332  tfi  7783  peano5  7823  resf1extb  7864  resf1ext2b  7865  xpord2pred  8075  frrlem12  8227  frrlem13  8228  tz7.48-1  8362  tz7.49  8364  dif20el  8420  oaf1o  8478  oeordi  8502  oeord  8503  oecan  8504  oeword  8505  oeworde  8508  oelimcl  8515  oeeulem  8516  oeeui  8517  oaabs2  8564  boxcutc  8865  domdifsn  8973  pssnn  9078  isinf  9149  pwfilem  9202  fsuppco2  9287  fsuppcor  9288  ordtypelem7  9410  unxpwdom2  9474  inf3lem3  9520  cantnfp1lem1  9568  cantnfp1lem3  9570  ttrcltr  9606  infxpenc2lem1  9910  dfacacn  10033  isf32lem3  10246  isf34lem4  10268  fin67  10286  isfin7-2  10287  domtriomlem  10333  axdc2lem  10339  axdc3lem4  10344  axdc4lem  10346  ttukeylem7  10406  konigthlem  10459  fpwwe2lem12  10533  fpwwe2  10534  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  chnccat  18532  chnrev  18533  grpinvnzcl  18924  symgextfv  19330  pmtrf  19367  pmtrdifellem3  19390  sylow2alem2  19530  sylow2a  19531  efgsf  19641  efgsrel  19646  efgs1  19647  efgsfo  19651  gsumzaddlem  19833  gsumzadd  19834  gsumzmhm  19849  gsum2d2lem  19885  dprdfadd  19934  dprdres  19942  subgdmdprd  19948  dmdprdsplitlem  19951  dmdprdsplit2lem  19959  dpjidcl  19972  ablfac1b  19984  pgpfac1lem1  19988  gsummgp0  20236  isirred  20337  irredrmul  20345  ringelnzr  20438  c0rhm  20449  c0rnghm  20450  zrrnghm  20451  zrinitorngc  20557  zrtermorngc  20558  isdomn2  20626  isdomn4  20631  isdrng2  20658  drngmcl  20665  isdrngd  20680  isdrngdOLD  20682  imadrhmcl  20712  cntzsdrg  20717  lcomfsupp  20835  lbspropd  21033  lspsneq  21059  lsppratlem6  21089  lbsextlem2  21096  lbsextlem4  21098  cnsubrg  21364  xrs1mnd  21377  xrs10  21378  xrs1cmn  21379  psgnodpm  21525  zrhpsgnodpm  21529  evpmodpmf1o  21533  uvcresum  21730  frlmssuvc1  21731  frlmsslsp  21733  frlmup2  21736  lindfrn  21758  f1lindf  21759  lindfmm  21764  islindf4  21775  psrbaglesupp  21859  psrlidm  21899  psrridm  21900  mplsubglem  21936  mpllsslem  21937  mplsubrglem  21941  mplmonmul  21971  mplcoe1  21972  mplcoe5  21975  mplbas2  21977  evlslem3  22015  mhpvscacl  22069  psdmul  22081  coe1tmmul2  22190  coe1tmmul  22191  dmatmul  22412  1marepvsma1  22498  mdetdiaglem  22513  mdetrlin  22517  mdetrsca  22518  mdetralt  22523  maducoeval2  22555  madugsum  22558  symgmatr01  22569  gsummatr01lem3  22572  gsummatr01lem4  22573  gsummatr01  22574  smadiadetlem0  22576  smadiadetlem1a  22578  cmpfi  23323  2ndcdisj2  23372  elptr2  23489  ptcnplem  23536  xkopt  23570  kqdisj  23647  fin1aufil  23847  ptcmplem2  23968  ptcmplem3  23969  ptcmplem4  23970  opnsubg  24023  lpbl  24418  blcld  24420  zcld  24729  recld2  24730  reconnlem1  24742  divcnOLD  24784  divcn  24786  iundisj  25476  mbfeqalem1  25569  itg1val2  25612  itg1ge0  25614  i1fmullem  25622  i1fadd  25623  itg1addlem4  25627  itg1mulc  25632  itg1lea  25640  itg1le  25641  mbfi1fseqlem4  25646  itg2uba  25671  itg2lea  25672  itg2eqa  25673  itg2splitlem  25676  itg2split  25677  itgeqa  25742  ellimc3  25807  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvcobr  25876  dvcobrOLD  25877  dvcjbr  25880  dvrec  25886  dvrecg  25904  dvcnvlem  25907  dvexp3  25909  dveflem  25910  tdeglem4  25992  deg1n0ima  26021  deg1mul3le  26049  ig1peu  26107  ply1termlem  26135  plypf1  26144  plyaddlem1  26145  plymullem1  26146  coeeulem  26156  coeidlem  26169  coeid3  26172  coefv0  26180  coemulhi  26186  coemulc  26187  dvply1  26218  fta1  26243  vieta1lem2  26246  elaa  26251  elqaalem2  26255  aannenlem2  26264  aaliou2  26275  tayl0  26296  dvtaylp  26305  taylthlem1  26308  taylthlem2  26309  taylthlem2OLD  26310  pserdvlem2  26365  logbcl  26704  relogbreexp  26712  relogbcxp  26722  cxplogb  26723  dcubic  26783  rlimcnp  26902  jensen  26926  dmgmaddn0  26960  dmlogdmgm  26961  lgamgulmlem2  26967  igamz  26985  gamp1  26995  regamcl  26998  wilthlem2  27006  basellem3  27020  chpub  27158  logexprlim  27163  lgslem1  27235  lgslem4  27238  lgsvalmod  27254  lgsqr  27289  lgsqrmod  27290  lgsqrmodndvds  27291  gausslemma2dlem0b  27295  gausslemma2dlem0c  27296  gausslemma2dlem0i  27302  gausslemma2dlem1a  27303  gausslemma2dlem4  27307  gausslemma2dlem5a  27308  gausslemma2dlem7  27311  gausslemma2d  27312  lgsquad2  27324  m1lgs  27326  2lgsoddprm  27354  2sqreultblem  27386  dchrisum0fno1  27449  rplogsum  27465  ishpg  28737  elntg2  28963  umgrislfupgrlem  29100  usgruspgrb  29161  nbumgrvtx  29324  nbupgrres  29342  isuvtx  29373  cusgrexilem2  29420  cusgrexi  29421  structtocusgr  29424  cusgrres  29427  cusgrfilem2  29435  vtxdginducedm1  29522  cusconngr  30171  2pthfrgr  30264  frgrncvvdeq  30289  frgrwopreglem4  30295  frgrwopreglem5  30301  frgrwopreg  30303  frgrhash2wsp  30312  strlem1  32230  strlem3  32233  strlem4  32234  strlem5  32235  hstrlem3  32241  hstrlem4  32242  iundisjf  32569  suppss3  32706  iundisjfi  32778  suppssnn0  32787  ind0  32839  qsdrngi  33460  zringidom  33516  zringfrac  33519  irngnzply1  33704  qtophaus  33849  elzdif0  33993  measvunilem  34225  sibfof  34353  eulerpartlemb  34381  eulerpartlemf  34383  sseqf  34405  ballotlem5  34513  ballotlemi1  34516  ballotlemii  34517  ballotlemic  34520  ballotlem1c  34521  ballotlemscr  34532  ballotlemro  34536  ballotlemfg  34539  ballotlemfrc  34540  ballotlemfrceq  34542  ballotlemrinv0  34546  plymulx0  34560  signstfvn  34582  signsvfn  34595  bnj923  34780  bnj570  34917  bnj594  34924  fineqvnttrclselem1  35141  fineqvnttrclselem2  35142  fineqvnttrclselem3  35143  fineqvnttrclse  35144  subfacp1lem1  35223  satffunlem2lem1  35448  mrsubcn  35563  mrsubco  35565  circum  35718  dfon2lem6  35830  neibastop1  36403  bj-restn0b  37135  lindsadd  37652  lindsenlbs  37654  matunitlindflem1  37655  poimirlem24  37683  poimirlem25  37684  dvtan  37709  itg2addnclem2  37711  ftc1cnnc  37731  dvasin  37743  dvreasin  37745  dvreacos  37746  isdrngo2  37997  isdrngo3  37998  divrngidl  38067  isfldidl  38107  pridlc2  38111  pridlc3  38112  blockadjliftmap  38471  prter2  38979  lsateln0  39093  lsatlss  39094  lsmsat  39106  lsatcv0  39129  lsat0cv  39131  lcv1  39139  l1cvpat  39152  dih1dimatlem  41427  dihatexv2  41437  djhcvat42  41513  dihjat1lem  41526  dochsatshp  41549  lcfl6  41598  mapdrvallem2  41743  mapdpglem32  41803  idomnnzgmulnz  42225  aks6d1c5lem3  42229  aks6d1c5lem2  42230  deg1gprod  42232  sticksstones22  42260  unitscyglem4  42290  readvrec2  42453  readvrec  42454  readvcot  42456  evlsvvvallem  42653  evlsvvvallem2  42654  evlsvvval  42655  evlsbagval  42658  selvvvval  42677  evlselv  42679  evlsmhpvvval  42687  prjspertr  42697  prjsperref  42698  prjspersym  42699  prjspvs  42702  prjsprellsp  42703  dffltz  42726  irrapx1  42920  pell1234qrne0  42945  pell1234qrreccl  42946  pell1234qrmulcl  42947  pell14qrgt0  42951  pell1234qrdich  42953  pell14qrdich  42961  pell1qrge1  42962  pell1qr1  42963  pell1qrgap  42966  pell14qrgapw  42968  pellqrexplicit  42969  pellqrex  42971  pellfundge  42974  pellfundgt1  42975  setindtr  43116  kelac1  43155  mpaaeu  43242  flcidc  43262  deg1mhm  43292  onexoegt  43336  cantnfub  43413  cantnfresb  43416  succlg  43420  dflim5  43421  onmcl  43423  omabs2  43424  tfsconcatrev  43440  minregex2  43627  radcnvrat  44406  binomcxplemdvbinom  44445  disjiun2  45154  fiiuncl  45161  disjf1o  45287  difmapsn  45308  supminfxr2  45566  icoiccdif  45623  iccdificc  45638  fsumnncl  45671  fsumsupp0  45677  fprod0  45695  climrec  45702  islpcn  45736  lptre2pt  45737  limclner  45748  cnrefiisplem  45926  fprodcncf  45997  fperdvper  46016  dvdivcncf  46024  dvnmul  46040  dvmptfprodlem  46041  dvnprodlem2  46044  stoweidlem25  46122  stoweidlem28  46125  stoweidlem41  46138  stoweidlem44  46141  stoweidlem46  46143  stirlinglem5  46175  dirkercncflem1  46200  dirkercncflem2  46201  fourierdlem24  46228  fourierdlem62  46265  fouriersw  46328  fouriercn  46329  elaa2lem  46330  elaa2  46331  etransclem25  46356  etransclem35  46366  etransclem44  46375  sge0iunmptlemfi  46510  sge0fodjrnlem  46513  iundjiunlem  46556  meadjiunlem  46562  meaiininclem  46583  isomenndlem  46627  hsphoidmvle2  46682  hsphoidmvle  46683  hoidmv1lelem2  46689  hoidmvle  46697  ovnhoilem1  46698  hspdifhsp  46713  hspmbllem2  46724  ovnsubadd2lem  46742  ovolval4lem1  46746  preimagelt  46796  preimalegt  46797  chnsubseq  46977  fsummsndifre  47471  fsummmodsndifre  47473  odz2prm2pw  47662  fmtnoprmfac1lem  47663  fmtnoprmfac2lem1  47665  2pwp1prm  47688  lighneallem2  47705  lighneallem3  47706  lighneallem4  47709  bgoldbtbndlem2  47905  bgoldbtbndlem3  47906  bgoldbtbndlem4  47907  bgoldbtbnd  47908  isubgrvtxuhgr  47963  2zrngnmlid2  48356  mgpsumunsn  48460  mgpsumz  48461  mgpsumn  48462  lindslinindsimp1  48557  lindslinindsimp2  48563  lincresunit1  48577  lincresunit2  48578  lincresunit3lem1  48579  lincresunit3lem2  48580  lincresunit3  48581  lindssnlvec  48586  logcxp0  48635  relogbmulbexp  48661  relogbdivb  48662  dignn0fr  48701  rrxlinesc  48835  eenglngeehlnmlem1  48837  eenglngeehlnmlem2  48838