Theorem eldifi 4085

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 496	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵)

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

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 3444  df-dif 3906

This theorem is referenced by:  difss  4090  eqoreldif  4644  xpdifid  6136  tz7.7  6353  tfi  7807  peano5  7847  resf1extb  7888  resf1ext2b  7889  xpord2pred  8099  frrlem12  8251  frrlem13  8252  tz7.48-1  8386  tz7.49  8388  dif20el  8444  oaf1o  8502  oeordi  8527  oeord  8528  oecan  8529  oeword  8530  oeworde  8533  oelimcl  8540  oeeulem  8541  oeeui  8542  oaabs2  8589  boxcutc  8893  domdifsn  9002  pssnn  9107  isinf  9179  pwfilem  9232  fsuppco2  9320  fsuppcor  9321  ordtypelem7  9443  unxpwdom2  9507  inf3lem3  9553  cantnfp1lem1  9601  cantnfp1lem3  9603  ttrcltr  9639  infxpenc2lem1  9943  dfacacn  10066  isf32lem3  10279  isf34lem4  10301  fin67  10319  isfin7-2  10320  domtriomlem  10366  axdc2lem  10372  axdc3lem4  10377  axdc4lem  10379  ttukeylem7  10439  konigthlem  10493  fpwwe2lem12  10567  fpwwe2  10568  modfzo0difsn  13880  hashf1lem1  14392  hashle2prv  14415  rlimrege0  15516  rlimrecl  15517  sumrblem  15648  fsumcvg  15649  summolem2a  15652  fsumss  15662  fsumsplit1  15682  fsumless  15733  cvgcmpce  15755  binomlem  15766  incexclem  15773  incexc  15774  isumltss  15785  prodrblem  15866  fprodcvg  15867  prodmolem2a  15871  fprodss  15885  fprodn0f  15928  fprodeq0g  15931  fprodmodd  15934  rpnnen2lem10  16162  rpnnen2lem11  16163  sumeven  16328  sumodd  16329  lcmfunsnlem2  16581  oddprmge3  16641  oddprm  16752  nnoddn2prm  16753  nnoddn2prmb  16755  iserodd  16777  prmreclem2  16859  prmreclem3  16860  prmreclem5  16862  4sqlem19  16905  prmdvdsprmo  16984  prmodvdslcmf  16989  prmlem0  17047  firest  17366  chnccat  18563  chnrev  18564  grpinvnzcl  18958  symgextfv  19364  pmtrf  19401  pmtrdifellem3  19424  sylow2alem2  19564  sylow2a  19565  efgsf  19675  efgsrel  19680  efgs1  19681  efgsfo  19685  gsumzaddlem  19867  gsumzadd  19868  gsumzmhm  19883  gsum2d2lem  19919  dprdfadd  19968  dprdres  19976  subgdmdprd  19982  dmdprdsplitlem  19985  dmdprdsplit2lem  19993  dpjidcl  20006  ablfac1b  20018  pgpfac1lem1  20022  gsummgp0  20270  isirred  20372  irredrmul  20380  ringelnzr  20473  c0rhm  20484  c0rnghm  20485  zrrnghm  20486  zrinitorngc  20592  zrtermorngc  20593  isdomn2  20661  isdomn4  20666  isdrng2  20693  drngmcl  20700  isdrngd  20715  isdrngdOLD  20717  imadrhmcl  20747  cntzsdrg  20752  lcomfsupp  20870  lbspropd  21068  lspsneq  21094  lsppratlem6  21124  lbsextlem2  21131  lbsextlem4  21133  cnsubrg  21399  xrs1mnd  21412  xrs10  21413  xrs1cmn  21414  psgnodpm  21560  zrhpsgnodpm  21564  evpmodpmf1o  21568  uvcresum  21765  frlmssuvc1  21766  frlmsslsp  21768  frlmup2  21771  lindfrn  21793  f1lindf  21794  lindfmm  21799  islindf4  21810  psrbaglesupp  21895  psrlidm  21934  psrridm  21935  mplsubglem  21971  mpllsslem  21972  mplsubrglem  21976  mplmonmul  22008  mplcoe1  22009  mplcoe5  22012  mplbas2  22014  evlslem3  22052  evlsvvvallem  22063  evlsvvvallem2  22064  evlsvvval  22065  mhpvscacl  22114  psdmul  22126  coe1tmmul2  22235  coe1tmmul  22236  dmatmul  22458  1marepvsma1  22544  mdetdiaglem  22559  mdetrlin  22563  mdetrsca  22564  mdetralt  22569  maducoeval2  22601  madugsum  22604  symgmatr01  22615  gsummatr01lem3  22618  gsummatr01lem4  22619  gsummatr01  22620  smadiadetlem0  22622  smadiadetlem1a  22624  cmpfi  23369  2ndcdisj2  23418  elptr2  23535  ptcnplem  23582  xkopt  23616  kqdisj  23693  fin1aufil  23893  ptcmplem2  24014  ptcmplem3  24015  ptcmplem4  24016  opnsubg  24069  lpbl  24464  blcld  24466  zcld  24775  recld2  24776  reconnlem1  24788  divcnOLD  24830  divcn  24832  iundisj  25522  mbfeqalem1  25615  itg1val2  25658  itg1ge0  25660  i1fmullem  25668  i1fadd  25669  itg1addlem4  25673  itg1mulc  25678  itg1lea  25686  itg1le  25687  mbfi1fseqlem4  25692  itg2uba  25717  itg2lea  25718  itg2eqa  25719  itg2splitlem  25722  itg2split  25723  itgeqa  25788  ellimc3  25853  dvaddbr  25913  dvmulbr  25914  dvmulbrOLD  25915  dvcobr  25922  dvcobrOLD  25923  dvcjbr  25926  dvrec  25932  dvrecg  25950  dvcnvlem  25953  dvexp3  25955  dveflem  25956  tdeglem4  26038  deg1n0ima  26067  deg1mul3le  26095  ig1peu  26153  ply1termlem  26181  plypf1  26190  plyaddlem1  26191  plymullem1  26192  coeeulem  26202  coeidlem  26215  coeid3  26218  coefv0  26226  coemulhi  26232  coemulc  26233  dvply1  26264  fta1  26289  vieta1lem2  26292  elaa  26297  elqaalem2  26301  aannenlem2  26310  aaliou2  26321  tayl0  26342  dvtaylp  26351  taylthlem1  26354  taylthlem2  26355  taylthlem2OLD  26356  pserdvlem2  26411  logbcl  26750  relogbreexp  26758  relogbcxp  26768  cxplogb  26769  dcubic  26829  rlimcnp  26948  jensen  26972  dmgmaddn0  27006  dmlogdmgm  27007  lgamgulmlem2  27013  igamz  27031  gamp1  27041  regamcl  27044  wilthlem2  27052  basellem3  27066  chpub  27204  logexprlim  27209  lgslem1  27281  lgslem4  27284  lgsvalmod  27300  lgsqr  27335  lgsqrmod  27336  lgsqrmodndvds  27337  gausslemma2dlem0b  27341  gausslemma2dlem0c  27342  gausslemma2dlem0i  27348  gausslemma2dlem1a  27349  gausslemma2dlem4  27353  gausslemma2dlem5a  27354  gausslemma2dlem7  27357  gausslemma2d  27358  lgsquad2  27370  m1lgs  27372  2lgsoddprm  27400  2sqreultblem  27432  dchrisum0fno1  27495  rplogsum  27511  ishpg  28849  elntg2  29076  umgrislfupgrlem  29213  usgruspgrb  29274  nbumgrvtx  29437  nbupgrres  29455  isuvtx  29486  cusgrexilem2  29533  cusgrexi  29534  structtocusgr  29537  cusgrres  29540  cusgrfilem2  29548  vtxdginducedm1  29635  cusconngr  30284  2pthfrgr  30377  frgrncvvdeq  30402  frgrwopreglem4  30408  frgrwopreglem5  30414  frgrwopreg  30416  frgrhash2wsp  30425  strlem1  32344  strlem3  32347  strlem4  32348  strlem5  32349  hstrlem3  32355  hstrlem4  32356  iundisjf  32682  suppss3  32819  iundisjfi  32893  suppssnn0  32902  ind0  32954  qsdrngi  33594  zringidom  33650  zringfrac  33653  psrmonmul  33733  irngnzply1  33875  qtophaus  34020  elzdif0  34164  measvunilem  34396  sibfof  34524  eulerpartlemb  34552  eulerpartlemf  34554  sseqf  34576  ballotlem5  34684  ballotlemi1  34687  ballotlemii  34688  ballotlemic  34691  ballotlem1c  34692  ballotlemscr  34703  ballotlemro  34707  ballotlemfg  34710  ballotlemfrc  34711  ballotlemfrceq  34713  ballotlemrinv0  34717  plymulx0  34731  signstfvn  34753  signsvfn  34766  bnj923  34951  bnj570  35087  bnj594  35094  fineqvnttrclselem1  35305  fineqvnttrclselem2  35306  fineqvnttrclselem3  35307  fineqvnttrclse  35308  subfacp1lem1  35401  satffunlem2lem1  35626  mrsubcn  35741  mrsubco  35743  circum  35896  dfon2lem6  36008  neibastop1  36581  bj-restn0b  37371  lindsadd  37893  lindsenlbs  37895  matunitlindflem1  37896  poimirlem24  37924  poimirlem25  37925  dvtan  37950  itg2addnclem2  37952  ftc1cnnc  37972  dvasin  37984  dvreasin  37986  dvreacos  37987  isdrngo2  38238  isdrngo3  38239  divrngidl  38308  isfldidl  38348  pridlc2  38352  pridlc3  38353  blockadjliftmap  38738  prter2  39286  lsateln0  39400  lsatlss  39401  lsmsat  39413  lsatcv0  39436  lsat0cv  39438  lcv1  39446  l1cvpat  39459  dih1dimatlem  41734  dihatexv2  41744  djhcvat42  41820  dihjat1lem  41833  dochsatshp  41856  lcfl6  41905  mapdrvallem2  42050  mapdpglem32  42110  idomnnzgmulnz  42532  aks6d1c5lem3  42536  aks6d1c5lem2  42537  deg1gprod  42539  sticksstones22  42567  unitscyglem4  42597  readvrec2  42760  readvrec  42761  readvcot  42763  evlsbagval  42956  selvvvval  42972  evlselv  42974  evlsmhpvvval  42982  prjspertr  42992  prjsperref  42993  prjspersym  42994  prjspvs  42997  prjsprellsp  42998  dffltz  43021  irrapx1  43214  pell1234qrne0  43239  pell1234qrreccl  43240  pell1234qrmulcl  43241  pell14qrgt0  43245  pell1234qrdich  43247  pell14qrdich  43255  pell1qrge1  43256  pell1qr1  43257  pell1qrgap  43260  pell14qrgapw  43262  pellqrexplicit  43263  pellqrex  43265  pellfundge  43268  pellfundgt1  43269  setindtr  43410  kelac1  43449  mpaaeu  43536  flcidc  43556  deg1mhm  43586  onexoegt  43630  cantnfub  43707  cantnfresb  43710  succlg  43714  dflim5  43715  onmcl  43717  omabs2  43718  tfsconcatrev  43734  minregex2  43920  radcnvrat  44699  binomcxplemdvbinom  44738  disjiun2  45447  fiiuncl  45454  disjf1o  45579  difmapsn  45599  supminfxr2  45856  icoiccdif  45913  iccdificc  45928  fsumnncl  45961  fsumsupp0  45967  fprod0  45985  climrec  45992  islpcn  46026  lptre2pt  46027  limclner  46038  cnrefiisplem  46216  fprodcncf  46287  fperdvper  46306  dvdivcncf  46314  dvnmul  46330  dvmptfprodlem  46331  dvnprodlem2  46334  stoweidlem25  46412  stoweidlem28  46415  stoweidlem41  46428  stoweidlem44  46431  stoweidlem46  46433  stirlinglem5  46465  dirkercncflem1  46490  dirkercncflem2  46491  fourierdlem24  46518  fourierdlem62  46555  fouriersw  46618  fouriercn  46619  elaa2lem  46620  elaa2  46621  etransclem25  46646  etransclem35  46656  etransclem44  46665  sge0iunmptlemfi  46800  sge0fodjrnlem  46803  iundjiunlem  46846  meadjiunlem  46852  meaiininclem  46873  isomenndlem  46917  hsphoidmvle2  46972  hsphoidmvle  46973  hoidmv1lelem2  46979  hoidmvle  46987  ovnhoilem1  46988  hspdifhsp  47003  hspmbllem2  47014  ovnsubadd2lem  47032  ovolval4lem1  47036  preimagelt  47086  preimalegt  47087  chnsubseq  47267  fsummsndifre  47761  fsummmodsndifre  47763  odz2prm2pw  47952  fmtnoprmfac1lem  47953  fmtnoprmfac2lem1  47955  2pwp1prm  47978  lighneallem2  47995  lighneallem3  47996  lighneallem4  47999  bgoldbtbndlem2  48195  bgoldbtbndlem3  48196  bgoldbtbndlem4  48197  bgoldbtbnd  48198  isubgrvtxuhgr  48253  2zrngnmlid2  48646  mgpsumunsn  48750  mgpsumz  48751  mgpsumn  48752  lindslinindsimp1  48846  lindslinindsimp2  48852  lincresunit1  48866  lincresunit2  48867  lincresunit3lem1  48868  lincresunit3lem2  48869  lincresunit3  48870  lindssnlvec  48875  logcxp0  48924  relogbmulbexp  48950  relogbdivb  48951  dignn0fr  48990  rrxlinesc  49124  eenglngeehlnmlem1  49126  eenglngeehlnmlem2  49127