Theorem eldifi 4070

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-dif 4050

This theorem is used by:  difss  4075  eqoreldif  4646  xpdifid  6170  xpdifcnvepel  6171  tz7.7  6403  tfi  7885  peano5  7926  resf1extb  7967  resf1ext2b  7968  xpord2pred  8186  frrlem12  8340  frrlem13  8341  tz7.48-1  8478  tz7.49  8480  dif20el  8538  oaf1o  8596  oeordi  8621  oeord  8622  oecan  8623  oeword  8624  oeworde  8627  oelimcl  8634  oeeulem  8635  oeeui  8636  oaabs2  8683  boxcutc  8994  domdifsn  9104  pssnn  9209  isinf  9281  pwfilem  9334  fsuppco2  9419  fsuppcor  9420  ordtypelem7  9542  unxpwdom2  9606  inf3lem3  9655  cantnfp1lem1  9703  cantnfp1lem3  9705  ttrcltr  9741  elhf3OLD  9947  infxpenc2lem1  10122  dfacacn  10244  isf32lem3  10457  isf34lem4  10479  fin67  10497  isfin7-2  10498  domtriomlem  10544  axdc2lem  10550  axdc3lem4  10555  axdc4lem  10557  ttukeylem7  10617  konigthlem  10677  fpwwe2lem12  10751  fpwwe2  10752  ind0  12354  modfzo0difsn  14110  hashf1lem1  14624  hashle2prv  14647  rlimrege0  15772  rlimrecl  15773  sumrblem  15903  fsumcvg  15904  summolem2a  15907  fsumss  15917  fsumsplit1  15937  fsumless  15989  cvgcmpce  16011  binomlem  16024  incexclem  16031  incexc  16032  isumltss  16043  prodrblem  16122  fprodcvg  16123  prodmolem2a  16127  fprodss  16141  fprodn0f  16184  fprodeq0g  16187  fprodmodd  16190  rpnnen2lem10  16417  rpnnen2lem11  16418  sumeven  16583  sumodd  16584  lcmfunsnlem2  16841  oddprmge3  16902  oddprm  17014  nnoddn2prm  17015  nnoddn2prmb  17017  iserodd  17039  prmreclem2  17121  prmreclem3  17122  prmreclem5  17124  4sqlem19  17167  prmdvdsprmo  17246  prmodvdslcmf  17251  prmlem0  17309  firest  17629  chnccat  18826  chnrev  18827  grpinvnzcl  19247  symgextfv  19659  pmtrf  19696  pmtrdifellem3  19719  sylow2alem2  19859  sylow2a  19860  efgsf  19970  efgsrel  19975  efgs1  19976  efgsfo  19980  gsumzaddlem  20162  gsumzadd  20163  gsumzmhm  20178  gsum2d2lem  20214  dprdfadd  20263  dprdres  20271  subgdmdprd  20277  dmdprdsplitlem  20280  dmdprdsplit2lem  20288  dpjidcl  20301  ablfac1b  20313  pgpfac1lem1  20317  gsummgp0  20574  isirred  20676  irredrmul  20684  ringelnzr  20801  c0rhm  20813  c0rnghm  20814  zrrnghm  20815  zrinitorngc  20921  zrtermorngc  20922  isdomn2  20990  isdomn4  20994  isdrng2  21024  isdrng3lem2  21033  isdrng5  21035  drngmcl  21036  isdrngd  21049  isdrngdOLD  21051  imadrhmcl  21081  cntzsdrg  21086  lcomfsupp  21204  lbspropd  21401  lspsneq  21427  lsppratlem6  21457  lbsextlem2  21464  lbsextlem4  21466  prmidlc2  21657  cmprmidlmcl  21658  cnsubrg  21760  xrs1mnd  21773  xrs10  21774  xrs1cmn  21775  psgnodpm  21921  zrhpsgnodpm  21925  evpmodpmf1o  21929  uvcresum  22126  frlmssuvc1  22127  frlmsslsp  22129  frlmup2  22132  lindfrn  22154  f1lindf  22155  lindfmm  22160  islindf4  22171  lindsenlbs  22184  psrbaglesupp  22257  psrlidm  22296  psrridm  22297  mplsubglem  22333  mpllsslem  22334  mplsubrglem  22338  mplmonmul  22372  mplcoe1  22373  mplcoe5  22376  mplbas2  22378  evlslem3  22416  evlsvvvallem  22427  evlsvvvallem2  22428  evlsvvval  22429  selvvvval  22478  mhpvscacl  22502  psdmul  22514  coe1tmmul2  22622  coe1tmmul  22623  dmatmul  22839  1marepvsma1  22925  mdetdiaglem  22940  mdetrlin  22944  mdetrsca  22945  mdetralt  22950  maducoeval2  22982  madugsum  22985  symgmatr01  22996  gsummatr01lem3  22999  gsummatr01lem4  23000  gsummatr01  23001  smadiadetlem0  23003  smadiadetlem1a  23005  matunitlindflem1  23021  cmpfi  23753  2ndcdisj2  23803  elptr2  23920  ptcnplem  23967  xkopt  24001  kqdisj  24078  fin1aufil  24278  ptcmplem2  24399  ptcmplem3  24400  ptcmplem4  24401  opnsubg  24454  lpbl  24849  blcld  24851  zcld  25160  recld2  25161  reconnlem1  25173  divcn  25216  iundisj  25896  mbfeqalem1  25989  itg1val2  26032  itg1ge0  26034  i1fmullem  26042  i1fadd  26043  itg1addlem4  26047  itg1mulc  26052  itg1lea  26060  itg1le  26061  mbfi1fseqlem4  26066  itg2uba  26091  itg2lea  26092  itg2eqa  26093  itg2splitlem  26096  itg2split  26097  itgeqa  26161  ellimc3  26226  dvaddbr  26285  dvmulbr  26286  dvcobr  26293  dvcjbr  26296  dvrec  26302  dvrecg  26320  dvcnvlem  26323  dvexp3  26325  dveflem  26326  tdeglem4  26405  deg1n0ima  26434  deg1mul3le  26462  ig1peu  26520  ply1termlem  26548  plypf1  26558  plyaddlem1  26559  plymullem1  26560  coeeulem  26570  coeidlem  26583  coeid3  26586  coefv0  26594  coemulhi  26600  coemulc  26601  plyn0mulidp  26629  dvply1  26632  fta1  26656  vieta1lem2  26661  elaa  26666  elqaalem2  26670  preimaaa  26673  aannenlem2  26683  aaliou2  26694  tayl0  26716  dvtaylp  26724  taylthlem1  26727  taylthlem2  26728  pserdvlem2  26782  logbcl  27122  relogbreexp  27130  relogbcxp  27140  cxplogb  27141  dcubic  27201  rlimcnp  27320  jensen  27343  dmgmaddn0  27377  dmlogdmgm  27378  lgamgulmlem2  27384  igamz  27402  gamp1  27412  regamcl  27415  wilthlem2  27423  basellem3  27437  chpub  27574  logexprlim  27579  lgslem1  27651  lgslem4  27654  lgsvalmod  27670  lgsqr  27705  lgsqrmod  27706  lgsqrmodndvds  27707  gausslemma2dlem0b  27711  gausslemma2dlem0c  27712  gausslemma2dlem0i  27718  gausslemma2dlem1a  27719  gausslemma2dlem4  27723  gausslemma2dlem5a  27724  gausslemma2dlem7  27727  gausslemma2d  27728  lgsquad2  27740  m1lgs  27742  2lgsoddprm  27770  2sqreultblem  27802  dchrisum0fno1  27865  rplogsum  27881  ishpg  29264  elntg2  29590  umgrislfupgrlem  29727  usgruspgrb  29791  nbumgrvtx  29954  nbupgrres  29972  isuvtx  30003  cusgrexilem2  30050  cusgrexi  30051  structtocusgr  30054  cusgrres  30056  cusgrfilem2  30064  vtxdginducedm1  30151  cusconngr  30819  2pthfrgr  30912  frgrncvvdeq  30937  frgrwopreglem4  30943  frgrwopreglem5  30949  frgrwopreg  30951  frgrhash2wsp  30960  strlem1  32879  strlem3  32882  strlem4  32883  strlem5  32884  hstrlem3  32890  hstrlem4  32891  iundisjf  33252  suppss3  33382  iundisjfi  33455  suppssnn0  33464  qsdrngi  34086  zringidom  34150  zringfrac  34153  psrmonmul  34249  irngnzply1  34390  qtophaus  34535  elzdif0  34679  measvunilem  34912  sibfof  35039  eulerpartlemb  35067  eulerpartlemf  35069  sseqf  35091  ballotlem5  35199  ballotlemi1  35202  ballotlemii  35203  ballotlemic  35206  ballotlem1c  35207  ballotlemscr  35218  ballotlemro  35222  ballotlemfg  35225  ballotlemfrc  35226  ballotlemfrceq  35228  ballotlemrinv0  35232  signstfvn  35265  signsvfn  35278  bnj923  35466  bnj570  35602  bnj594  35609  acwer1prc  35851  fineqvnttrclselem1  35888  fineqvnttrclselem2  35889  fineqvnttrclselem3  35890  fineqvnttrclse  35891  subfacp1lem1  36110  satffunlem2lem1  36335  mrsubcn  36450  mrsubco  36452  circum  36605  dfon2lem6  36727  neibastop1  37324  bj-restn0b  38202  lindsadd  38727  poimirlem24  38753  poimirlem25  38754  dvtan  38779  itg2addnclem2  38781  ftc1cnnc  38801  dvasin  38813  dvreasin  38815  dvreacos  38816  isdrngo2  39083  isdrngo3  39084  divrngidl  39153  isfldidl  39193  pridlc2  39197  pridlc3  39198  blockadjliftmap  39581  prter2  40129  lsateln0  40243  lsatlss  40244  lsmsat  40256  lsatcv0  40279  lsat0cv  40281  lcv1  40289  l1cvpat  40302  dih1dimatlem  42577  dihatexv2  42587  djhcvat42  42663  dihjat1lem  42676  dochsatshp  42699  lcfl6  42748  mapdrvallem2  42893  mapdpglem32  42953  idomnnzgmulnz  43374  aks6d1c5lem3  43378  aks6d1c5lem2  43379  deg1gprod  43381  sticksstones22  43409  unitscyglem4  43439  readvrec2  43603  readvrec  43604  readvcot  43606  evlsbagval  43805  evlselv  43808  evlsmhpvvval  43814  prjspertr  43824  prjsperref  43825  prjspersym  43826  prjspvs  43829  prjsprellsp  43830  dffltz  43861  irrapx1  44026  pell1234qrne0  44051  pell1234qrreccl  44052  pell1234qrmulcl  44053  pell14qrgt0  44057  pell1234qrdich  44059  pell14qrdich  44067  pell1qrge1  44068  pell1qr1  44069  pell1qrgap  44072  pell14qrgapw  44074  pellqrexplicit  44075  pellqrex  44077  pellfundge  44080  pellfundgt1  44081  setindtr  44222  kelac1  44256  mpaaeu  44342  flcidc  44362  deg1mhm  44392  onexoegt  44436  cantnfub  44513  cantnfresb  44516  succlg  44520  dflim5  44521  onmcl  44523  omabs2  44524  tfsconcatrev  44540  minregex2  44726  radcnvrat  45488  binomcxplemdvbinom  45527  disjiun2  46278  fiiuncl  46285  disjf1o  46409  difmapsn  46428  supminfxr2  46682  icoiccdif  46739  iccdificc  46754  fsumnncl  46787  fsumsupp0  46793  fprod0  46811  climrec  46818  islpcn  46852  lptre2pt  46853  limclner  46864  cnrefiisplem  47042  fprodcncf  47113  fperdvper  47132  dvdivcncf  47140  dvnmul  47156  dvmptfprodlem  47157  dvnprodlem2  47160  stoweidlem25  47238  stoweidlem28  47241  stoweidlem41  47254  stoweidlem44  47257  stoweidlem46  47259  stirlinglem5  47291  dirkercncflem1  47316  dirkercncflem2  47317  fourierdlem24  47344  fourierdlem62  47381  fouriersw  47444  fouriercn  47445  elaa2lem  47446  elaa2  47447  etransclem25  47472  etransclem35  47482  etransclem44  47491  sge0iunmptlemfi  47626  sge0fodjrnlem  47629  iundjiunlem  47672  meadjiunlem  47678  meaiininclem  47699  isomenndlem  47743  hsphoidmvle2  47798  hsphoidmvle  47799  hoidmv1lelem2  47805  hoidmvle  47813  ovnhoilem1  47814  hspdifhsp  47829  hspmbllem2  47840  ovnsubadd2lem  47858  ovolval4lem1  47862  preimagelt  47912  preimalegt  47913  chnsubseq  48093  tmachlem-tpopen  48154  fsummsndifre  48653  fsummmodsndifre  48655  odz2prm2pw  48851  fmtnoprmfac1lem  48852  fmtnoprmfac2lem1  48854  2pwp1prm  48877  lighneallem2  48894  lighneallem3  48895  lighneallem4  48898  bgoldbtbndlem2  49107  bgoldbtbndlem3  49108  bgoldbtbndlem4  49109  bgoldbtbnd  49110  isubgrvtxuhgr  49165  2zrngnmlid2  49557  mgpsumunsn  49676  mgpsumz  49677  mgpsumn  49678  lindslinindsimp1  49772  lindslinindsimp2  49778  lincresunit1  49792  lincresunit2  49793  lincresunit3lem1  49794  lincresunit3lem2  49795  lincresunit3  49796  lindssnlvec  49801  logcxp0  49850  relogbmulbexp  49876  relogbdivb  49877  dignn0fr  49916  rrxlinesc  50051  eenglngeehlnmlem1  50053  eenglngeehlnmlem2  50054