Theorem eldifi 4072

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

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

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 3432  df-dif 3893

This theorem is referenced by:  difss  4077  eqoreldif  4630  xpdifid  6128  tz7.7  6345  tfi  7799  peano5  7839  resf1extb  7880  resf1ext2b  7881  xpord2pred  8090  frrlem12  8242  frrlem13  8243  tz7.48-1  8377  tz7.49  8379  dif20el  8435  oaf1o  8493  oeordi  8518  oeord  8519  oecan  8520  oeword  8521  oeworde  8524  oelimcl  8531  oeeulem  8532  oeeui  8533  oaabs2  8580  boxcutc  8884  domdifsn  8993  pssnn  9098  isinf  9170  pwfilem  9223  fsuppco2  9311  fsuppcor  9312  ordtypelem7  9434  unxpwdom2  9498  inf3lem3  9546  cantnfp1lem1  9594  cantnfp1lem3  9596  ttrcltr  9632  infxpenc2lem1  9936  dfacacn  10059  isf32lem3  10272  isf34lem4  10294  fin67  10312  isfin7-2  10313  domtriomlem  10359  axdc2lem  10365  axdc3lem4  10370  axdc4lem  10372  ttukeylem7  10432  konigthlem  10486  fpwwe2lem12  10560  fpwwe2  10561  ind0  12164  modfzo0difsn  13900  hashf1lem1  14412  hashle2prv  14435  rlimrege0  15536  rlimrecl  15537  sumrblem  15668  fsumcvg  15669  summolem2a  15672  fsumss  15682  fsumsplit1  15702  fsumless  15754  cvgcmpce  15776  binomlem  15789  incexclem  15796  incexc  15797  isumltss  15808  prodrblem  15889  fprodcvg  15890  prodmolem2a  15894  fprodss  15908  fprodn0f  15951  fprodeq0g  15954  fprodmodd  15957  rpnnen2lem10  16185  rpnnen2lem11  16186  sumeven  16351  sumodd  16352  lcmfunsnlem2  16604  oddprmge3  16665  oddprm  16776  nnoddn2prm  16777  nnoddn2prmb  16779  iserodd  16801  prmreclem2  16883  prmreclem3  16884  prmreclem5  16886  4sqlem19  16929  prmdvdsprmo  17008  prmodvdslcmf  17013  prmlem0  17071  firest  17390  chnccat  18587  chnrev  18588  grpinvnzcl  18982  symgextfv  19388  pmtrf  19425  pmtrdifellem3  19448  sylow2alem2  19588  sylow2a  19589  efgsf  19699  efgsrel  19704  efgs1  19705  efgsfo  19709  gsumzaddlem  19891  gsumzadd  19892  gsumzmhm  19907  gsum2d2lem  19943  dprdfadd  19992  dprdres  20000  subgdmdprd  20006  dmdprdsplitlem  20009  dmdprdsplit2lem  20017  dpjidcl  20030  ablfac1b  20042  pgpfac1lem1  20046  gsummgp0  20292  isirred  20394  irredrmul  20402  ringelnzr  20495  c0rhm  20506  c0rnghm  20507  zrrnghm  20508  zrinitorngc  20614  zrtermorngc  20615  isdomn2  20683  isdomn4  20688  isdrng2  20715  drngmcl  20722  isdrngd  20737  isdrngdOLD  20739  imadrhmcl  20769  cntzsdrg  20774  lcomfsupp  20892  lbspropd  21090  lspsneq  21116  lsppratlem6  21146  lbsextlem2  21153  lbsextlem4  21155  cnsubrg  21421  xrs1mnd  21434  xrs10  21435  xrs1cmn  21436  psgnodpm  21582  zrhpsgnodpm  21586  evpmodpmf1o  21590  uvcresum  21787  frlmssuvc1  21788  frlmsslsp  21790  frlmup2  21793  lindfrn  21815  f1lindf  21816  lindfmm  21821  islindf4  21832  psrbaglesupp  21916  psrlidm  21954  psrridm  21955  mplsubglem  21991  mpllsslem  21992  mplsubrglem  21996  mplmonmul  22028  mplcoe1  22029  mplcoe5  22032  mplbas2  22034  evlslem3  22072  evlsvvvallem  22083  evlsvvvallem2  22084  evlsvvval  22085  mhpvscacl  22134  psdmul  22146  coe1tmmul2  22255  coe1tmmul  22256  dmatmul  22476  1marepvsma1  22562  mdetdiaglem  22577  mdetrlin  22581  mdetrsca  22582  mdetralt  22587  maducoeval2  22619  madugsum  22622  symgmatr01  22633  gsummatr01lem3  22636  gsummatr01lem4  22637  gsummatr01  22638  smadiadetlem0  22640  smadiadetlem1a  22642  cmpfi  23387  2ndcdisj2  23436  elptr2  23553  ptcnplem  23600  xkopt  23634  kqdisj  23711  fin1aufil  23911  ptcmplem2  24032  ptcmplem3  24033  ptcmplem4  24034  opnsubg  24087  lpbl  24482  blcld  24484  zcld  24793  recld2  24794  reconnlem1  24806  divcn  24849  iundisj  25529  mbfeqalem1  25622  itg1val2  25665  itg1ge0  25667  i1fmullem  25675  i1fadd  25676  itg1addlem4  25680  itg1mulc  25685  itg1lea  25693  itg1le  25694  mbfi1fseqlem4  25699  itg2uba  25724  itg2lea  25725  itg2eqa  25726  itg2splitlem  25729  itg2split  25730  itgeqa  25795  ellimc3  25860  dvaddbr  25919  dvmulbr  25920  dvcobr  25927  dvcjbr  25930  dvrec  25936  dvrecg  25954  dvcnvlem  25957  dvexp3  25959  dveflem  25960  tdeglem4  26039  deg1n0ima  26068  deg1mul3le  26096  ig1peu  26154  ply1termlem  26182  plypf1  26191  plyaddlem1  26192  plymullem1  26193  coeeulem  26203  coeidlem  26216  coeid3  26219  coefv0  26227  coemulhi  26233  coemulc  26234  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  26410  logbcl  26748  relogbreexp  26756  relogbcxp  26766  cxplogb  26767  dcubic  26827  rlimcnp  26946  jensen  26970  dmgmaddn0  27004  dmlogdmgm  27005  lgamgulmlem2  27011  igamz  27029  gamp1  27039  regamcl  27042  wilthlem2  27050  basellem3  27064  chpub  27201  logexprlim  27206  lgslem1  27278  lgslem4  27281  lgsvalmod  27297  lgsqr  27332  lgsqrmod  27333  lgsqrmodndvds  27334  gausslemma2dlem0b  27338  gausslemma2dlem0c  27339  gausslemma2dlem0i  27345  gausslemma2dlem1a  27346  gausslemma2dlem4  27350  gausslemma2dlem5a  27351  gausslemma2dlem7  27354  gausslemma2d  27355  lgsquad2  27367  m1lgs  27369  2lgsoddprm  27397  2sqreultblem  27429  dchrisum0fno1  27492  rplogsum  27508  ishpg  28845  elntg2  29072  umgrislfupgrlem  29209  usgruspgrb  29270  nbumgrvtx  29433  nbupgrres  29451  isuvtx  29482  cusgrexilem2  29529  cusgrexi  29530  structtocusgr  29533  cusgrres  29536  cusgrfilem2  29544  vtxdginducedm1  29631  cusconngr  30280  2pthfrgr  30373  frgrncvvdeq  30398  frgrwopreglem4  30404  frgrwopreglem5  30410  frgrwopreg  30412  frgrhash2wsp  30421  strlem1  32340  strlem3  32343  strlem4  32344  strlem5  32345  hstrlem3  32351  hstrlem4  32352  iundisjf  32678  suppss3  32815  iundisjfi  32888  suppssnn0  32897  qsdrngi  33574  zringidom  33630  zringfrac  33633  psrmonmul  33713  irngnzply1  33855  qtophaus  34000  elzdif0  34144  measvunilem  34376  sibfof  34504  eulerpartlemb  34532  eulerpartlemf  34534  sseqf  34556  ballotlem5  34664  ballotlemi1  34667  ballotlemii  34668  ballotlemic  34671  ballotlem1c  34672  ballotlemscr  34683  ballotlemro  34687  ballotlemfg  34690  ballotlemfrc  34691  ballotlemfrceq  34693  ballotlemrinv0  34697  plymulx0  34711  signstfvn  34733  signsvfn  34746  bnj923  34931  bnj570  35067  bnj594  35074  fineqvnttrclselem1  35285  fineqvnttrclselem2  35286  fineqvnttrclselem3  35287  fineqvnttrclse  35288  subfacp1lem1  35381  satffunlem2lem1  35606  mrsubcn  35721  mrsubco  35723  circum  35876  dfon2lem6  35988  neibastop1  36561  bj-restn0b  37423  lindsadd  37954  lindsenlbs  37956  matunitlindflem1  37957  poimirlem24  37985  poimirlem25  37986  dvtan  38011  itg2addnclem2  38013  ftc1cnnc  38033  dvasin  38045  dvreasin  38047  dvreacos  38048  isdrngo2  38299  isdrngo3  38300  divrngidl  38369  isfldidl  38409  pridlc2  38413  pridlc3  38414  blockadjliftmap  38799  prter2  39347  lsateln0  39461  lsatlss  39462  lsmsat  39474  lsatcv0  39497  lsat0cv  39499  lcv1  39507  l1cvpat  39520  dih1dimatlem  41795  dihatexv2  41805  djhcvat42  41881  dihjat1lem  41894  dochsatshp  41917  lcfl6  41966  mapdrvallem2  42111  mapdpglem32  42171  idomnnzgmulnz  42592  aks6d1c5lem3  42596  aks6d1c5lem2  42597  deg1gprod  42599  sticksstones22  42627  unitscyglem4  42657  readvrec2  42813  readvrec  42814  readvcot  42816  evlsbagval  43022  selvvvval  43038  evlselv  43040  evlsmhpvvval  43048  prjspertr  43058  prjsperref  43059  prjspersym  43060  prjspvs  43063  prjsprellsp  43064  dffltz  43087  irrapx1  43280  pell1234qrne0  43305  pell1234qrreccl  43306  pell1234qrmulcl  43307  pell14qrgt0  43311  pell1234qrdich  43313  pell14qrdich  43321  pell1qrge1  43322  pell1qr1  43323  pell1qrgap  43326  pell14qrgapw  43328  pellqrexplicit  43329  pellqrex  43331  pellfundge  43334  pellfundgt1  43335  setindtr  43476  kelac1  43515  mpaaeu  43602  flcidc  43622  deg1mhm  43652  onexoegt  43696  cantnfub  43773  cantnfresb  43776  succlg  43780  dflim5  43781  onmcl  43783  omabs2  43784  tfsconcatrev  43800  minregex2  43986  radcnvrat  44765  binomcxplemdvbinom  44804  disjiun2  45513  fiiuncl  45520  disjf1o  45645  difmapsn  45665  supminfxr2  45921  icoiccdif  45978  iccdificc  45993  fsumnncl  46026  fsumsupp0  46032  fprod0  46050  climrec  46057  islpcn  46091  lptre2pt  46092  limclner  46103  cnrefiisplem  46281  fprodcncf  46352  fperdvper  46371  dvdivcncf  46379  dvnmul  46395  dvmptfprodlem  46396  dvnprodlem2  46399  stoweidlem25  46477  stoweidlem28  46480  stoweidlem41  46493  stoweidlem44  46496  stoweidlem46  46498  stirlinglem5  46530  dirkercncflem1  46555  dirkercncflem2  46556  fourierdlem24  46583  fourierdlem62  46620  fouriersw  46683  fouriercn  46684  elaa2lem  46685  elaa2  46686  etransclem25  46711  etransclem35  46721  etransclem44  46730  sge0iunmptlemfi  46865  sge0fodjrnlem  46868  iundjiunlem  46911  meadjiunlem  46917  meaiininclem  46938  isomenndlem  46982  hsphoidmvle2  47037  hsphoidmvle  47038  hoidmv1lelem2  47044  hoidmvle  47052  ovnhoilem1  47053  hspdifhsp  47068  hspmbllem2  47079  ovnsubadd2lem  47097  ovolval4lem1  47101  preimagelt  47151  preimalegt  47152  chnsubseq  47332  fsummsndifre  47846  fsummmodsndifre  47848  odz2prm2pw  48044  fmtnoprmfac1lem  48045  fmtnoprmfac2lem1  48047  2pwp1prm  48070  lighneallem2  48087  lighneallem3  48088  lighneallem4  48091  bgoldbtbndlem2  48300  bgoldbtbndlem3  48301  bgoldbtbndlem4  48302  bgoldbtbnd  48303  isubgrvtxuhgr  48358  2zrngnmlid2  48751  mgpsumunsn  48855  mgpsumz  48856  mgpsumn  48857  lindslinindsimp1  48951  lindslinindsimp2  48957  lincresunit1  48971  lincresunit2  48972  lincresunit3lem1  48973  lincresunit3lem2  48974  lincresunit3  48975  lindssnlvec  48980  logcxp0  49029  relogbmulbexp  49055  relogbdivb  49056  dignn0fr  49095  rrxlinesc  49229  eenglngeehlnmlem1  49231  eenglngeehlnmlem2  49232