Theorem eldifi 4084

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-dif 3907

This theorem is used by:  difss  4089  eqoreldif  4650  xpdifid  6164  xpdifcnvepel  6165  tz7.7  6386  tfi  7847  peano5  7888  resf1extb  7929  resf1ext2b  7930  xpord2pred  8139  frrlem12  8292  frrlem13  8293  tz7.48-1  8428  tz7.49  8430  dif20el  8488  oaf1o  8546  oeordi  8571  oeord  8572  oecan  8573  oeword  8574  oeworde  8577  oelimcl  8584  oeeulem  8585  oeeui  8586  oaabs2  8633  boxcutc  8937  domdifsn  9046  pssnn  9151  isinf  9223  pwfilem  9275  fsuppco2  9361  fsuppcor  9362  ordtypelem7  9484  unxpwdom2  9548  inf3lem3  9597  cantnfp1lem1  9645  cantnfp1lem3  9647  ttrcltr  9683  infxpenc2lem1  10010  dfacacn  10132  isf32lem3  10345  isf34lem4  10367  fin67  10385  isfin7-2  10386  domtriomlem  10432  axdc2lem  10438  axdc3lem4  10443  axdc4lem  10445  ttukeylem7  10505  konigthlem  10559  fpwwe2lem12  10633  fpwwe2  10634  ind0  12234  modfzo0difsn  13986  hashf1lem1  14499  hashle2prv  14522  rlimrege0  15637  rlimrecl  15638  sumrblem  15769  fsumcvg  15770  summolem2a  15773  fsumss  15783  fsumsplit1  15803  fsumless  15855  cvgcmpce  15877  binomlem  15890  incexclem  15897  incexc  15898  isumltss  15909  prodrblem  15990  fprodcvg  15991  prodmolem2a  15995  fprodss  16009  fprodn0f  16052  fprodeq0g  16055  fprodmodd  16058  rpnnen2lem10  16285  rpnnen2lem11  16286  sumeven  16451  sumodd  16452  lcmfunsnlem2  16704  oddprmge3  16765  oddprm  16876  nnoddn2prm  16877  nnoddn2prmb  16879  iserodd  16901  prmreclem2  16983  prmreclem3  16984  prmreclem5  16986  4sqlem19  17029  prmdvdsprmo  17108  prmodvdslcmf  17113  prmlem0  17171  firest  17491  chnccat  18688  chnrev  18689  grpinvnzcl  19083  symgextfv  19494  pmtrf  19531  pmtrdifellem3  19554  sylow2alem2  19694  sylow2a  19695  efgsf  19805  efgsrel  19810  efgs1  19811  efgsfo  19815  gsumzaddlem  19997  gsumzadd  19998  gsumzmhm  20013  gsum2d2lem  20049  dprdfadd  20098  dprdres  20106  subgdmdprd  20112  dmdprdsplitlem  20115  dmdprdsplit2lem  20123  dpjidcl  20136  ablfac1b  20148  pgpfac1lem1  20152  gsummgp0  20406  isirred  20508  irredrmul  20516  ringelnzr  20632  c0rhm  20644  c0rnghm  20645  zrrnghm  20646  zrinitorngc  20752  zrtermorngc  20753  isdomn2  20821  isdomn4  20825  isdrng2  20854  isdrng3lem2  20863  isdrng5  20865  drngmcl  20866  isdrngd  20879  isdrngdOLD  20881  imadrhmcl  20911  cntzsdrg  20916  lcomfsupp  21034  lbspropd  21231  lspsneq  21257  lsppratlem6  21287  lbsextlem2  21294  lbsextlem4  21296  prmidlc2  21485  cmprmidlmcl  21486  cnsubrg  21588  xrs1mnd  21601  xrs10  21602  xrs1cmn  21603  psgnodpm  21749  zrhpsgnodpm  21753  evpmodpmf1o  21757  uvcresum  21954  frlmssuvc1  21955  frlmsslsp  21957  frlmup2  21960  lindfrn  21982  f1lindf  21983  lindfmm  21988  islindf4  21999  psrbaglesupp  22083  psrlidm  22122  psrridm  22123  mplsubglem  22159  mpllsslem  22160  mplsubrglem  22164  mplmonmul  22198  mplcoe1  22199  mplcoe5  22202  mplbas2  22204  evlslem3  22242  evlsvvvallem  22253  evlsvvvallem2  22254  evlsvvval  22255  selvvvval  22304  mhpvscacl  22328  psdmul  22340  coe1tmmul2  22448  coe1tmmul  22449  dmatmul  22665  1marepvsma1  22751  mdetdiaglem  22766  mdetrlin  22770  mdetrsca  22771  mdetralt  22776  maducoeval2  22808  madugsum  22811  symgmatr01  22822  gsummatr01lem3  22825  gsummatr01lem4  22826  gsummatr01  22827  smadiadetlem0  22829  smadiadetlem1a  22831  cmpfi  23576  2ndcdisj2  23625  elptr2  23742  ptcnplem  23789  xkopt  23823  kqdisj  23900  fin1aufil  24100  ptcmplem2  24221  ptcmplem3  24222  ptcmplem4  24223  opnsubg  24276  lpbl  24671  blcld  24673  zcld  24982  recld2  24983  reconnlem1  24995  divcn  25038  iundisj  25718  mbfeqalem1  25811  itg1val2  25854  itg1ge0  25856  i1fmullem  25864  i1fadd  25865  itg1addlem4  25869  itg1mulc  25874  itg1lea  25882  itg1le  25883  mbfi1fseqlem4  25888  itg2uba  25913  itg2lea  25914  itg2eqa  25915  itg2splitlem  25918  itg2split  25919  itgeqa  25984  ellimc3  26049  dvaddbr  26108  dvmulbr  26109  dvcobr  26116  dvcjbr  26119  dvrec  26125  dvrecg  26143  dvcnvlem  26146  dvexp3  26148  dveflem  26149  tdeglem4  26228  deg1n0ima  26257  deg1mul3le  26285  ig1peu  26343  ply1termlem  26371  plypf1  26380  plyaddlem1  26381  plymullem1  26382  coeeulem  26392  coeidlem  26405  coeid3  26408  coefv0  26416  coemulhi  26422  coemulc  26423  plyn0mulidp  26453  dvply1  26456  fta1  26480  vieta1lem2  26483  elaa  26488  elqaalem2  26492  aannenlem2  26503  aaliou2  26514  tayl0  26536  dvtaylp  26544  taylthlem1  26547  taylthlem2  26548  pserdvlem2  26602  logbcl  26943  relogbreexp  26951  relogbcxp  26961  cxplogb  26962  dcubic  27022  rlimcnp  27141  jensen  27164  dmgmaddn0  27198  dmlogdmgm  27199  lgamgulmlem2  27205  igamz  27223  gamp1  27233  regamcl  27236  wilthlem2  27244  basellem3  27258  chpub  27395  logexprlim  27400  lgslem1  27472  lgslem4  27475  lgsvalmod  27491  lgsqr  27526  lgsqrmod  27527  lgsqrmodndvds  27528  gausslemma2dlem0b  27532  gausslemma2dlem0c  27533  gausslemma2dlem0i  27539  gausslemma2dlem1a  27540  gausslemma2dlem4  27544  gausslemma2dlem5a  27545  gausslemma2dlem7  27548  gausslemma2d  27549  lgsquad2  27561  m1lgs  27563  2lgsoddprm  27591  2sqreultblem  27623  dchrisum0fno1  27686  rplogsum  27702  ishpg  29052  elntg2  29346  umgrislfupgrlem  29483  usgruspgrb  29544  nbumgrvtx  29707  nbupgrres  29725  isuvtx  29756  cusgrexilem2  29803  cusgrexi  29804  structtocusgr  29807  cusgrres  29809  cusgrfilem2  29817  vtxdginducedm1  29904  cusconngr  30553  2pthfrgr  30646  frgrncvvdeq  30671  frgrwopreglem4  30677  frgrwopreglem5  30683  frgrwopreg  30685  frgrhash2wsp  30694  strlem1  32613  strlem3  32616  strlem4  32617  strlem5  32618  hstrlem3  32624  hstrlem4  32625  iundisjf  32945  suppss3  33079  iundisjfi  33152  suppssnn0  33161  qsdrngi  33786  zringidom  33850  zringfrac  33853  psrmonmul  33949  irngnzply1  34090  qtophaus  34235  elzdif0  34379  measvunilem  34611  sibfof  34739  eulerpartlemb  34767  eulerpartlemf  34769  sseqf  34791  ballotlem5  34899  ballotlemi1  34902  ballotlemii  34903  ballotlemic  34906  ballotlem1c  34907  ballotlemscr  34918  ballotlemro  34922  ballotlemfg  34925  ballotlemfrc  34926  ballotlemfrceq  34928  ballotlemrinv0  34932  signstfvn  34965  signsvfn  34978  bnj923  35166  bnj570  35302  bnj594  35309  fineqvnttrclselem1  35542  fineqvnttrclselem2  35543  fineqvnttrclselem3  35544  fineqvnttrclse  35545  subfacp1lem1  35679  satffunlem2lem1  35904  mrsubcn  36019  mrsubco  36021  circum  36174  dfon2lem6  36286  neibastop1  36898  bj-restn0b  37761  lindsadd  38292  lindsenlbs  38294  matunitlindflem1  38295  poimirlem24  38323  poimirlem25  38324  dvtan  38349  itg2addnclem2  38351  ftc1cnnc  38371  dvasin  38383  dvreasin  38385  dvreacos  38386  isdrngo2  38637  isdrngo3  38638  divrngidl  38707  isfldidl  38747  pridlc2  38751  pridlc3  38752  blockadjliftmap  39135  prter2  39683  lsateln0  39797  lsatlss  39798  lsmsat  39810  lsatcv0  39833  lsat0cv  39835  lcv1  39843  l1cvpat  39856  dih1dimatlem  42131  dihatexv2  42141  djhcvat42  42217  dihjat1lem  42230  dochsatshp  42253  lcfl6  42302  mapdrvallem2  42447  mapdpglem32  42507  idomnnzgmulnz  42928  aks6d1c5lem3  42932  aks6d1c5lem2  42933  deg1gprod  42935  sticksstones22  42963  unitscyglem4  42993  readvrec2  43150  readvrec  43151  readvcot  43153  evlsbagval  43346  evlselv  43349  evlsmhpvvval  43355  prjspertr  43365  prjsperref  43366  prjspersym  43367  prjspvs  43370  prjsprellsp  43371  dffltz  43394  irrapx1  43583  pell1234qrne0  43608  pell1234qrreccl  43609  pell1234qrmulcl  43610  pell14qrgt0  43614  pell1234qrdich  43616  pell14qrdich  43624  pell1qrge1  43625  pell1qr1  43626  pell1qrgap  43629  pell14qrgapw  43631  pellqrexplicit  43632  pellqrex  43634  pellfundge  43637  pellfundgt1  43638  setindtr  43779  kelac1  43818  mpaaeu  43905  flcidc  43925  deg1mhm  43955  onexoegt  43999  cantnfub  44076  cantnfresb  44079  succlg  44083  dflim5  44084  onmcl  44086  omabs2  44087  tfsconcatrev  44103  minregex2  44289  radcnvrat  45052  binomcxplemdvbinom  45091  disjiun2  45806  fiiuncl  45813  disjf1o  45937  difmapsn  45956  supminfxr2  46211  icoiccdif  46268  iccdificc  46283  fsumnncl  46316  fsumsupp0  46322  fprod0  46340  climrec  46347  islpcn  46381  lptre2pt  46382  limclner  46393  cnrefiisplem  46571  fprodcncf  46642  fperdvper  46661  dvdivcncf  46669  dvnmul  46685  dvmptfprodlem  46686  dvnprodlem2  46689  stoweidlem25  46767  stoweidlem28  46770  stoweidlem41  46783  stoweidlem44  46786  stoweidlem46  46788  stirlinglem5  46820  dirkercncflem1  46845  dirkercncflem2  46846  fourierdlem24  46873  fourierdlem62  46910  fouriersw  46973  fouriercn  46974  elaa2lem  46975  elaa2  46976  etransclem25  47001  etransclem35  47011  etransclem44  47020  sge0iunmptlemfi  47155  sge0fodjrnlem  47158  iundjiunlem  47201  meadjiunlem  47207  meaiininclem  47228  isomenndlem  47272  hsphoidmvle2  47327  hsphoidmvle  47328  hoidmv1lelem2  47334  hoidmvle  47342  ovnhoilem1  47343  hspdifhsp  47358  hspmbllem2  47369  ovnsubadd2lem  47387  ovolval4lem1  47391  preimagelt  47441  preimalegt  47442  chnsubseq  47624  fsummsndifre  48145  fsummmodsndifre  48147  odz2prm2pw  48343  fmtnoprmfac1lem  48344  fmtnoprmfac2lem1  48346  2pwp1prm  48369  lighneallem2  48386  lighneallem3  48387  lighneallem4  48390  bgoldbtbndlem2  48599  bgoldbtbndlem3  48600  bgoldbtbndlem4  48601  bgoldbtbnd  48602  isubgrvtxuhgr  48657  2zrngnmlid2  49050  mgpsumunsn  49169  mgpsumz  49170  mgpsumn  49171  lindslinindsimp1  49265  lindslinindsimp2  49271  lincresunit1  49285  lincresunit2  49286  lincresunit3lem1  49287  lincresunit3lem2  49288  lincresunit3  49289  lindssnlvec  49294  logcxp0  49343  relogbmulbexp  49369  relogbdivb  49370  dignn0fr  49409  rrxlinesc  49543  eenglngeehlnmlem1  49545  eenglngeehlnmlem2  49546