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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145   ∖ cdif 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3900

This theorem is used by:  difss  4083  eqoreldif  4646  xpdifid  6159  xpdifcnvepel  6160  tz7.7  6389  tfi  7865  peano5  7906  resf1extb  7947  resf1ext2b  7948  xpord2pred  8163  frrlem12  8316  frrlem13  8317  tz7.48-1  8454  tz7.49  8456  dif20el  8514  oaf1o  8572  oeordi  8597  oeord  8598  oecan  8599  oeword  8600  oeworde  8603  oelimcl  8610  oeeulem  8611  oeeui  8612  oaabs2  8659  boxcutc  8970  domdifsn  9080  pssnn  9185  isinf  9257  pwfilem  9310  fsuppco2  9396  fsuppcor  9397  ordtypelem7  9519  unxpwdom2  9583  inf3lem3  9632  cantnfp1lem1  9680  cantnfp1lem3  9682  ttrcltr  9718  elhf3OLD  9924  infxpenc2lem1  10099  dfacacn  10221  isf32lem3  10434  isf34lem4  10456  fin67  10474  isfin7-2  10475  domtriomlem  10521  axdc2lem  10527  axdc3lem4  10532  axdc4lem  10534  ttukeylem7  10594  konigthlem  10654  fpwwe2lem12  10728  fpwwe2  10729  ind0  12331  modfzo0difsn  14087  hashf1lem1  14601  hashle2prv  14624  rlimrege0  15747  rlimrecl  15748  sumrblem  15878  fsumcvg  15879  summolem2a  15882  fsumss  15892  fsumsplit1  15912  fsumless  15964  cvgcmpce  15986  binomlem  15999  incexclem  16006  incexc  16007  isumltss  16018  prodrblem  16097  fprodcvg  16098  prodmolem2a  16102  fprodss  16116  fprodn0f  16159  fprodeq0g  16162  fprodmodd  16165  rpnnen2lem10  16392  rpnnen2lem11  16393  sumeven  16558  sumodd  16559  lcmfunsnlem2  16816  oddprmge3  16877  oddprm  16989  nnoddn2prm  16990  nnoddn2prmb  16992  iserodd  17014  prmreclem2  17096  prmreclem3  17097  prmreclem5  17099  4sqlem19  17142  prmdvdsprmo  17221  prmodvdslcmf  17226  prmlem0  17284  firest  17604  chnccat  18801  chnrev  18802  grpinvnzcl  19222  symgextfv  19633  pmtrf  19670  pmtrdifellem3  19693  sylow2alem2  19833  sylow2a  19834  efgsf  19944  efgsrel  19949  efgs1  19950  efgsfo  19954  gsumzaddlem  20136  gsumzadd  20137  gsumzmhm  20152  gsum2d2lem  20188  dprdfadd  20237  dprdres  20245  subgdmdprd  20251  dmdprdsplitlem  20254  dmdprdsplit2lem  20262  dpjidcl  20275  ablfac1b  20287  pgpfac1lem1  20291  gsummgp0  20548  isirred  20650  irredrmul  20658  ringelnzr  20775  c0rhm  20787  c0rnghm  20788  zrrnghm  20789  zrinitorngc  20895  zrtermorngc  20896  isdomn2  20964  isdomn4  20968  isdrng2  20998  isdrng3lem2  21007  isdrng5  21009  drngmcl  21010  isdrngd  21023  isdrngdOLD  21025  imadrhmcl  21055  cntzsdrg  21060  lcomfsupp  21178  lbspropd  21375  lspsneq  21401  lsppratlem6  21431  lbsextlem2  21438  lbsextlem4  21440  prmidlc2  21631  cmprmidlmcl  21632  cnsubrg  21734  xrs1mnd  21747  xrs10  21748  xrs1cmn  21749  psgnodpm  21895  zrhpsgnodpm  21899  evpmodpmf1o  21903  uvcresum  22100  frlmssuvc1  22101  frlmsslsp  22103  frlmup2  22106  lindfrn  22128  f1lindf  22129  lindfmm  22134  islindf4  22145  lindsenlbs  22158  psrbaglesupp  22231  psrlidm  22270  psrridm  22271  mplsubglem  22307  mpllsslem  22308  mplsubrglem  22312  mplmonmul  22346  mplcoe1  22347  mplcoe5  22350  mplbas2  22352  evlslem3  22390  evlsvvvallem  22401  evlsvvvallem2  22402  evlsvvval  22403  selvvvval  22452  mhpvscacl  22476  psdmul  22488  coe1tmmul2  22596  coe1tmmul  22597  dmatmul  22813  1marepvsma1  22899  mdetdiaglem  22914  mdetrlin  22918  mdetrsca  22919  mdetralt  22924  maducoeval2  22956  madugsum  22959  symgmatr01  22970  gsummatr01lem3  22973  gsummatr01lem4  22974  gsummatr01  22975  smadiadetlem0  22977  smadiadetlem1a  22979  matunitlindflem1  22995  cmpfi  23727  2ndcdisj2  23777  elptr2  23894  ptcnplem  23941  xkopt  23975  kqdisj  24052  fin1aufil  24252  ptcmplem2  24373  ptcmplem3  24374  ptcmplem4  24375  opnsubg  24428  lpbl  24823  blcld  24825  zcld  25134  recld2  25135  reconnlem1  25147  divcn  25190  iundisj  25870  mbfeqalem1  25963  itg1val2  26006  itg1ge0  26008  i1fmullem  26016  i1fadd  26017  itg1addlem4  26021  itg1mulc  26026  itg1lea  26034  itg1le  26035  mbfi1fseqlem4  26040  itg2uba  26065  itg2lea  26066  itg2eqa  26067  itg2splitlem  26070  itg2split  26071  itgeqa  26135  ellimc3  26200  dvaddbr  26259  dvmulbr  26260  dvcobr  26267  dvcjbr  26270  dvrec  26276  dvrecg  26294  dvcnvlem  26297  dvexp3  26299  dveflem  26300  tdeglem4  26379  deg1n0ima  26408  deg1mul3le  26436  ig1peu  26494  ply1termlem  26522  plypf1  26532  plyaddlem1  26533  plymullem1  26534  coeeulem  26544  coeidlem  26557  coeid3  26560  coefv0  26568  coemulhi  26574  coemulc  26575  plyn0mulidp  26603  dvply1  26606  fta1  26630  vieta1lem2  26635  elaa  26640  elqaalem2  26644  preimaaa  26647  aannenlem2  26657  aaliou2  26668  tayl0  26690  dvtaylp  26698  taylthlem1  26701  taylthlem2  26702  pserdvlem2  26756  logbcl  27096  relogbreexp  27104  relogbcxp  27114  cxplogb  27115  dcubic  27175  rlimcnp  27294  jensen  27317  dmgmaddn0  27351  dmlogdmgm  27352  lgamgulmlem2  27358  igamz  27376  gamp1  27386  regamcl  27389  wilthlem2  27397  basellem3  27411  chpub  27548  logexprlim  27553  lgslem1  27625  lgslem4  27628  lgsvalmod  27644  lgsqr  27679  lgsqrmod  27680  lgsqrmodndvds  27681  gausslemma2dlem0b  27685  gausslemma2dlem0c  27686  gausslemma2dlem0i  27692  gausslemma2dlem1a  27693  gausslemma2dlem4  27697  gausslemma2dlem5a  27698  gausslemma2dlem7  27701  gausslemma2d  27702  lgsquad2  27714  m1lgs  27716  2lgsoddprm  27744  2sqreultblem  27776  dchrisum0fno1  27839  rplogsum  27855  ishpg  29238  elntg2  29564  umgrislfupgrlem  29701  usgruspgrb  29765  nbumgrvtx  29928  nbupgrres  29946  isuvtx  29977  cusgrexilem2  30024  cusgrexi  30025  structtocusgr  30028  cusgrres  30030  cusgrfilem2  30038  vtxdginducedm1  30125  cusconngr  30793  2pthfrgr  30886  frgrncvvdeq  30911  frgrwopreglem4  30917  frgrwopreglem5  30923  frgrwopreg  30925  frgrhash2wsp  30934  strlem1  32853  strlem3  32856  strlem4  32857  strlem5  32858  hstrlem3  32864  hstrlem4  32865  iundisjf  33184  suppss3  33316  iundisjfi  33389  suppssnn0  33398  qsdrngi  34020  zringidom  34084  zringfrac  34087  psrmonmul  34183  irngnzply1  34324  qtophaus  34469  elzdif0  34613  measvunilem  34846  sibfof  34973  eulerpartlemb  35001  eulerpartlemf  35003  sseqf  35025  ballotlem5  35133  ballotlemi1  35136  ballotlemii  35137  ballotlemic  35140  ballotlem1c  35141  ballotlemscr  35152  ballotlemro  35156  ballotlemfg  35159  ballotlemfrc  35160  ballotlemfrceq  35162  ballotlemrinv0  35166  signstfvn  35199  signsvfn  35212  bnj923  35400  bnj570  35536  bnj594  35543  acwer1prc  35761  fineqvnttrclselem1  35790  fineqvnttrclselem2  35791  fineqvnttrclselem3  35792  fineqvnttrclse  35793  subfacp1lem1  35945  satffunlem2lem1  36170  mrsubcn  36285  mrsubco  36287  circum  36440  dfon2lem6  36551  neibastop1  37148  bj-restn0b  38013  lindsadd  38538  poimirlem24  38564  poimirlem25  38565  dvtan  38590  itg2addnclem2  38592  ftc1cnnc  38612  dvasin  38624  dvreasin  38626  dvreacos  38627  isdrngo2  38894  isdrngo3  38895  divrngidl  38964  isfldidl  39004  pridlc2  39008  pridlc3  39009  blockadjliftmap  39392  prter2  39940  lsateln0  40054  lsatlss  40055  lsmsat  40067  lsatcv0  40090  lsat0cv  40092  lcv1  40100  l1cvpat  40113  dih1dimatlem  42388  dihatexv2  42398  djhcvat42  42474  dihjat1lem  42487  dochsatshp  42510  lcfl6  42559  mapdrvallem2  42704  mapdpglem32  42764  idomnnzgmulnz  43185  aks6d1c5lem3  43189  aks6d1c5lem2  43190  deg1gprod  43192  sticksstones22  43220  unitscyglem4  43250  readvrec2  43414  readvrec  43415  readvcot  43417  evlsbagval  43616  evlselv  43619  evlsmhpvvval  43625  prjspertr  43635  prjsperref  43636  prjspersym  43637  prjspvs  43640  prjsprellsp  43641  dffltz  43672  irrapx1  43836  pell1234qrne0  43861  pell1234qrreccl  43862  pell1234qrmulcl  43863  pell14qrgt0  43867  pell1234qrdich  43869  pell14qrdich  43877  pell1qrge1  43878  pell1qr1  43879  pell1qrgap  43882  pell14qrgapw  43884  pellqrexplicit  43885  pellqrex  43887  pellfundge  43890  pellfundgt1  43891  setindtr  44032  kelac1  44066  mpaaeu  44153  flcidc  44173  deg1mhm  44203  onexoegt  44247  cantnfub  44324  cantnfresb  44327  succlg  44331  dflim5  44332  onmcl  44334  omabs2  44335  tfsconcatrev  44351  minregex2  44537  radcnvrat  45299  binomcxplemdvbinom  45338  disjiun2  46076  fiiuncl  46083  disjf1o  46207  difmapsn  46226  supminfxr2  46480  icoiccdif  46537  iccdificc  46552  fsumnncl  46585  fsumsupp0  46591  fprod0  46609  climrec  46616  islpcn  46650  lptre2pt  46651  limclner  46662  cnrefiisplem  46840  fprodcncf  46911  fperdvper  46930  dvdivcncf  46938  dvnmul  46954  dvmptfprodlem  46955  dvnprodlem2  46958  stoweidlem25  47036  stoweidlem28  47039  stoweidlem41  47052  stoweidlem44  47055  stoweidlem46  47057  stirlinglem5  47089  dirkercncflem1  47114  dirkercncflem2  47115  fourierdlem24  47142  fourierdlem62  47179  fouriersw  47242  fouriercn  47243  elaa2lem  47244  elaa2  47245  etransclem25  47270  etransclem35  47280  etransclem44  47289  sge0iunmptlemfi  47424  sge0fodjrnlem  47427  iundjiunlem  47470  meadjiunlem  47476  meaiininclem  47497  isomenndlem  47541  hsphoidmvle2  47596  hsphoidmvle  47597  hoidmv1lelem2  47603  hoidmvle  47611  ovnhoilem1  47612  hspdifhsp  47627  hspmbllem2  47638  ovnsubadd2lem  47656  ovolval4lem1  47660  preimagelt  47710  preimalegt  47711  chnsubseq  47891  tmachlem-tpopen  47952  fsummsndifre  48451  fsummmodsndifre  48453  odz2prm2pw  48649  fmtnoprmfac1lem  48650  fmtnoprmfac2lem1  48652  2pwp1prm  48675  lighneallem2  48692  lighneallem3  48693  lighneallem4  48696  bgoldbtbndlem2  48905  bgoldbtbndlem3  48906  bgoldbtbndlem4  48907  bgoldbtbnd  48908  isubgrvtxuhgr  48963  2zrngnmlid2  49355  mgpsumunsn  49474  mgpsumz  49475  mgpsumn  49476  lindslinindsimp1  49570  lindslinindsimp2  49576  lincresunit1  49590  lincresunit2  49591  lincresunit3lem1  49592  lincresunit3lem2  49593  lincresunit3  49594  lindssnlvec  49599  logcxp0  49648  relogbmulbexp  49674  relogbdivb  49675  dignn0fr  49714  rrxlinesc  49848  eenglngeehlnmlem1  49850  eenglngeehlnmlem2  49851