Theorem eldifi 4064

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2121   ∖ cdif 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-dif 3888

This theorem is referenced by:  difss  4069  eqoreldif  4620  xpdifid  6123  tz7.7  6340  tfi  7797  peano5  7837  resf1extb  7878  resf1ext2b  7879  xpord2pred  8089  frrlem12  8241  frrlem13  8242  tz7.48-1  8376  tz7.49  8378  dif20el  8434  oaf1o  8492  oeordi  8517  oeord  8518  oecan  8519  oeword  8520  oeworde  8523  oelimcl  8530  oeeulem  8531  oeeui  8532  oaabs2  8579  boxcutc  8883  domdifsn  8992  pssnn  9097  isinf  9169  pwfilem  9222  fsuppco2  9310  fsuppcor  9311  ordtypelem7  9433  unxpwdom2  9497  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  20499  c0rhm  20510  c0rnghm  20511  zrrnghm  20512  zrinitorngc  20618  zrtermorngc  20619  isdomn2  20687  isdomn4  20692  isdrng2  20719  drngmcl  20726  isdrngd  20741  isdrngdOLD  20743  imadrhmcl  20773  cntzsdrg  20778  lcomfsupp  20896  lbspropd  21093  lspsneq  21119  lsppratlem6  21149  lbsextlem2  21156  lbsextlem4  21158  cnsubrg  21406  xrs1mnd  21419  xrs10  21420  xrs1cmn  21421  psgnodpm  21567  zrhpsgnodpm  21571  evpmodpmf1o  21575  uvcresum  21772  frlmssuvc1  21773  frlmsslsp  21775  frlmup2  21778  lindfrn  21800  f1lindf  21801  lindfmm  21806  islindf4  21817  psrbaglesupp  21901  psrlidm  21940  psrridm  21941  mplsubglem  21977  mpllsslem  21978  mplsubrglem  21982  mplmonmul  22016  mplcoe1  22017  mplcoe5  22020  mplbas2  22022  evlslem3  22060  evlsvvvallem  22071  evlsvvvallem2  22072  evlsvvval  22073  selvvvval  22122  mhpvscacl  22146  psdmul  22158  coe1tmmul2  22266  coe1tmmul  22267  dmatmul  22484  1marepvsma1  22570  mdetdiaglem  22585  mdetrlin  22589  mdetrsca  22590  mdetralt  22595  maducoeval2  22627  madugsum  22630  symgmatr01  22641  gsummatr01lem3  22644  gsummatr01lem4  22645  gsummatr01  22646  smadiadetlem0  22648  smadiadetlem1a  22650  cmpfi  23395  2ndcdisj2  23444  elptr2  23561  ptcnplem  23608  xkopt  23642  kqdisj  23719  fin1aufil  23919  ptcmplem2  24040  ptcmplem3  24041  ptcmplem4  24042  opnsubg  24095  lpbl  24490  blcld  24492  zcld  24801  recld2  24802  reconnlem1  24814  divcn  24857  iundisj  25537  mbfeqalem1  25630  itg1val2  25673  itg1ge0  25675  i1fmullem  25683  i1fadd  25684  itg1addlem4  25688  itg1mulc  25693  itg1lea  25701  itg1le  25702  mbfi1fseqlem4  25707  itg2uba  25732  itg2lea  25733  itg2eqa  25734  itg2splitlem  25737  itg2split  25738  itgeqa  25803  ellimc3  25868  dvaddbr  25927  dvmulbr  25928  dvcobr  25935  dvcjbr  25938  dvrec  25944  dvrecg  25962  dvcnvlem  25965  dvexp3  25967  dveflem  25968  tdeglem4  26047  deg1n0ima  26076  deg1mul3le  26104  ig1peu  26162  ply1termlem  26190  plypf1  26199  plyaddlem1  26200  plymullem1  26201  coeeulem  26211  coeidlem  26224  coeid3  26227  coefv0  26235  coemulhi  26241  coemulc  26242  dvply1  26272  fta1  26296  vieta1lem2  26299  elaa  26304  elqaalem2  26308  aannenlem2  26317  aaliou2  26328  tayl0  26349  dvtaylp  26357  taylthlem1  26360  taylthlem2  26361  pserdvlem2  26415  logbcl  26753  relogbreexp  26761  relogbcxp  26771  cxplogb  26772  dcubic  26832  rlimcnp  26951  jensen  26974  dmgmaddn0  27008  dmlogdmgm  27009  lgamgulmlem2  27015  igamz  27033  gamp1  27043  regamcl  27046  wilthlem2  27054  basellem3  27068  chpub  27205  logexprlim  27210  lgslem1  27282  lgslem4  27285  lgsvalmod  27301  lgsqr  27336  lgsqrmod  27337  lgsqrmodndvds  27338  gausslemma2dlem0b  27342  gausslemma2dlem0c  27343  gausslemma2dlem0i  27349  gausslemma2dlem1a  27350  gausslemma2dlem4  27354  gausslemma2dlem5a  27355  gausslemma2dlem7  27358  gausslemma2d  27359  lgsquad2  27371  m1lgs  27373  2lgsoddprm  27401  2sqreultblem  27433  dchrisum0fno1  27496  rplogsum  27512  ishpg  28849  elntg2  29076  umgrislfupgrlem  29213  usgruspgrb  29274  nbumgrvtx  29437  nbupgrres  29455  isuvtx  29486  cusgrexilem2  29533  cusgrexi  29534  structtocusgr  29537  cusgrres  29539  cusgrfilem2  29547  vtxdginducedm1  29634  cusconngr  30283  2pthfrgr  30376  frgrncvvdeq  30401  frgrwopreglem4  30407  frgrwopreglem5  30413  frgrwopreg  30415  frgrhash2wsp  30424  strlem1  32343  strlem3  32346  strlem4  32347  strlem5  32348  hstrlem3  32354  hstrlem4  32355  iundisjf  32682  suppss3  32819  iundisjfi  32892  suppssnn0  32901  qsdrngi  33582  zringidom  33646  zringfrac  33649  psrmonmul  33746  irngnzply1  33887  qtophaus  34032  elzdif0  34176  measvunilem  34408  sibfof  34536  eulerpartlemb  34564  eulerpartlemf  34566  sseqf  34588  ballotlem5  34696  ballotlemi1  34699  ballotlemii  34700  ballotlemic  34703  ballotlem1c  34704  ballotlemscr  34715  ballotlemro  34719  ballotlemfg  34722  ballotlemfrc  34723  ballotlemfrceq  34725  ballotlemrinv0  34729  plymulx0  34743  signstfvn  34765  signsvfn  34778  bnj923  34966  bnj570  35102  bnj594  35109  fineqvnttrclselem1  35317  fineqvnttrclselem2  35318  fineqvnttrclselem3  35319  fineqvnttrclse  35320  subfacp1lem1  35422  satffunlem2lem1  35647  mrsubcn  35762  mrsubco  35764  circum  35917  dfon2lem6  36029  neibastop1  36602  bj-restn0b  37464  lindsadd  37995  lindsenlbs  37997  matunitlindflem1  37998  poimirlem24  38026  poimirlem25  38027  dvtan  38052  itg2addnclem2  38054  ftc1cnnc  38074  dvasin  38086  dvreasin  38088  dvreacos  38089  isdrngo2  38340  isdrngo3  38341  divrngidl  38410  isfldidl  38450  pridlc2  38454  pridlc3  38455  blockadjliftmap  38840  prter2  39388  lsateln0  39502  lsatlss  39503  lsmsat  39515  lsatcv0  39538  lsat0cv  39540  lcv1  39548  l1cvpat  39561  dih1dimatlem  41836  dihatexv2  41846  djhcvat42  41922  dihjat1lem  41935  dochsatshp  41958  lcfl6  42007  mapdrvallem2  42152  mapdpglem32  42212  idomnnzgmulnz  42633  aks6d1c5lem3  42637  aks6d1c5lem2  42638  deg1gprod  42640  sticksstones22  42668  unitscyglem4  42698  readvrec2  42853  readvrec  42854  readvcot  42856  evlsbagval  43051  evlselv  43054  evlsmhpvvval  43060  prjspertr  43070  prjsperref  43071  prjspersym  43072  prjspvs  43075  prjsprellsp  43076  dffltz  43099  irrapx1  43288  pell1234qrne0  43313  pell1234qrreccl  43314  pell1234qrmulcl  43315  pell14qrgt0  43319  pell1234qrdich  43321  pell14qrdich  43329  pell1qrge1  43330  pell1qr1  43331  pell1qrgap  43334  pell14qrgapw  43336  pellqrexplicit  43337  pellqrex  43339  pellfundge  43342  pellfundgt1  43343  setindtr  43484  kelac1  43523  mpaaeu  43610  flcidc  43630  deg1mhm  43660  onexoegt  43704  cantnfub  43781  cantnfresb  43784  succlg  43788  dflim5  43789  onmcl  43791  omabs2  43792  tfsconcatrev  43808  minregex2  43994  radcnvrat  44773  binomcxplemdvbinom  44812  disjiun2  45521  fiiuncl  45528  disjf1o  45652  difmapsn  45671  supminfxr2  45926  icoiccdif  45983  iccdificc  45998  fsumnncl  46031  fsumsupp0  46037  fprod0  46055  climrec  46062  islpcn  46096  lptre2pt  46097  limclner  46108  cnrefiisplem  46286  fprodcncf  46357  fperdvper  46376  dvdivcncf  46384  dvnmul  46400  dvmptfprodlem  46401  dvnprodlem2  46404  stoweidlem25  46482  stoweidlem28  46485  stoweidlem41  46498  stoweidlem44  46501  stoweidlem46  46503  stirlinglem5  46535  dirkercncflem1  46560  dirkercncflem2  46561  fourierdlem24  46588  fourierdlem62  46625  fouriersw  46688  fouriercn  46689  elaa2lem  46690  elaa2  46691  etransclem25  46716  etransclem35  46726  etransclem44  46735  sge0iunmptlemfi  46870  sge0fodjrnlem  46873  iundjiunlem  46916  meadjiunlem  46922  meaiininclem  46943  isomenndlem  46987  hsphoidmvle2  47042  hsphoidmvle  47043  hoidmv1lelem2  47049  hoidmvle  47057  ovnhoilem1  47058  hspdifhsp  47073  hspmbllem2  47084  ovnsubadd2lem  47102  ovolval4lem1  47106  preimagelt  47156  preimalegt  47157  chnsubseq  47339  fsummsndifre  47857  fsummmodsndifre  47859  odz2prm2pw  48055  fmtnoprmfac1lem  48056  fmtnoprmfac2lem1  48058  2pwp1prm  48081  lighneallem2  48098  lighneallem3  48099  lighneallem4  48102  bgoldbtbndlem2  48311  bgoldbtbndlem3  48312  bgoldbtbndlem4  48313  bgoldbtbnd  48314  isubgrvtxuhgr  48369  2zrngnmlid2  48762  mgpsumunsn  48866  mgpsumz  48867  mgpsumn  48868  lindslinindsimp1  48962  lindslinindsimp2  48968  lincresunit1  48982  lincresunit2  48983  lincresunit3lem1  48984  lincresunit3lem2  48985  lincresunit3  48986  lindssnlvec  48991  logcxp0  49040  relogbmulbexp  49066  relogbdivb  49067  dignn0fr  49106  rrxlinesc  49240  eenglngeehlnmlem1  49242  eenglngeehlnmlem2  49243