Theorem eldifi 4090

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   ∖ cdif 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914

This theorem is referenced by:  difss  4095  eqoreldif  4645  xpdifid  6129  tz7.7  6346  tfi  7809  peano5  7849  resf1extb  7890  resf1ext2b  7891  xpord2pred  8101  frrlem12  8253  frrlem13  8254  tz7.48-1  8388  tz7.49  8390  dif20el  8446  oaf1o  8504  oeordi  8528  oeord  8529  oecan  8530  oeword  8531  oeworde  8534  oelimcl  8541  oeeulem  8542  oeeui  8543  oaabs2  8590  boxcutc  8891  domdifsn  9001  pssnn  9109  isinf  9183  isinfOLD  9184  pwfilem  9243  fsuppco2  9330  fsuppcor  9331  ordtypelem7  9453  unxpwdom2  9517  inf3lem3  9559  cantnfp1lem1  9607  cantnfp1lem3  9609  ttrcltr  9645  infxpenc2lem1  9948  dfacacn  10071  isf32lem3  10284  isf34lem4  10306  fin67  10324  isfin7-2  10325  domtriomlem  10371  axdc2lem  10377  axdc3lem4  10382  axdc4lem  10384  ttukeylem7  10444  konigthlem  10497  fpwwe2lem12  10571  fpwwe2  10572  modfzo0difsn  13884  hashf1lem1  14396  hashle2prv  14419  rlimrege0  15521  rlimrecl  15522  sumrblem  15653  fsumcvg  15654  summolem2a  15657  fsumss  15667  fsumsplit1  15687  fsumless  15738  cvgcmpce  15760  binomlem  15771  incexclem  15778  incexc  15779  isumltss  15790  prodrblem  15871  fprodcvg  15872  prodmolem2a  15876  fprodss  15890  fprodn0f  15933  fprodeq0g  15936  fprodmodd  15939  rpnnen2lem10  16167  rpnnen2lem11  16168  sumeven  16333  sumodd  16334  lcmfunsnlem2  16586  oddprmge3  16646  oddprm  16757  nnoddn2prm  16758  nnoddn2prmb  16760  iserodd  16782  prmreclem2  16864  prmreclem3  16865  prmreclem5  16867  4sqlem19  16910  prmdvdsprmo  16989  prmodvdslcmf  16994  prmlem0  17052  firest  17371  grpinvnzcl  18925  symgextfv  19332  pmtrf  19369  pmtrdifellem3  19392  sylow2alem2  19532  sylow2a  19533  efgsf  19643  efgsrel  19648  efgs1  19649  efgsfo  19653  gsumzaddlem  19835  gsumzadd  19836  gsumzmhm  19851  gsum2d2lem  19887  dprdfadd  19936  dprdres  19944  subgdmdprd  19950  dmdprdsplitlem  19953  dmdprdsplit2lem  19961  dpjidcl  19974  ablfac1b  19986  pgpfac1lem1  19990  gsummgp0  20238  isirred  20339  irredrmul  20347  ringelnzr  20443  c0rhm  20454  c0rnghm  20455  zrrnghm  20456  zrinitorngc  20562  zrtermorngc  20563  isdomn2  20631  isdomn4  20636  isdrng2  20663  drngmcl  20670  isdrngd  20685  isdrngdOLD  20687  imadrhmcl  20717  cntzsdrg  20722  lcomfsupp  20840  lbspropd  21038  lspsneq  21064  lsppratlem6  21094  lbsextlem2  21101  lbsextlem4  21103  cnsubrg  21369  xrs1mnd  21382  xrs10  21383  xrs1cmn  21384  psgnodpm  21530  zrhpsgnodpm  21534  evpmodpmf1o  21538  uvcresum  21735  frlmssuvc1  21736  frlmsslsp  21738  frlmup2  21741  lindfrn  21763  f1lindf  21764  lindfmm  21769  islindf4  21780  psrbaglesupp  21864  psrlidm  21904  psrridm  21905  mplsubglem  21941  mpllsslem  21942  mplsubrglem  21946  mplmonmul  21976  mplcoe1  21977  mplcoe5  21980  mplbas2  21982  evlslem3  22020  mhpvscacl  22074  psdmul  22086  coe1tmmul2  22195  coe1tmmul  22196  dmatmul  22417  1marepvsma1  22503  mdetdiaglem  22518  mdetrlin  22522  mdetrsca  22523  mdetralt  22528  maducoeval2  22560  madugsum  22563  symgmatr01  22574  gsummatr01lem3  22577  gsummatr01lem4  22578  gsummatr01  22579  smadiadetlem0  22581  smadiadetlem1a  22583  cmpfi  23328  2ndcdisj2  23377  elptr2  23494  ptcnplem  23541  xkopt  23575  kqdisj  23652  fin1aufil  23852  ptcmplem2  23973  ptcmplem3  23974  ptcmplem4  23975  opnsubg  24028  lpbl  24424  blcld  24426  zcld  24735  recld2  24736  reconnlem1  24748  divcnOLD  24790  divcn  24792  iundisj  25482  mbfeqalem1  25575  itg1val2  25618  itg1ge0  25620  i1fmullem  25628  i1fadd  25629  itg1addlem4  25633  itg1mulc  25638  itg1lea  25646  itg1le  25647  mbfi1fseqlem4  25652  itg2uba  25677  itg2lea  25678  itg2eqa  25679  itg2splitlem  25682  itg2split  25683  itgeqa  25748  ellimc3  25813  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  dvcobr  25882  dvcobrOLD  25883  dvcjbr  25886  dvrec  25892  dvrecg  25910  dvcnvlem  25913  dvexp3  25915  dveflem  25916  tdeglem4  25998  deg1n0ima  26027  deg1mul3le  26055  ig1peu  26113  ply1termlem  26141  plypf1  26150  plyaddlem1  26151  plymullem1  26152  coeeulem  26162  coeidlem  26175  coeid3  26178  coefv0  26186  coemulhi  26192  coemulc  26193  dvply1  26224  fta1  26249  vieta1lem2  26252  elaa  26257  elqaalem2  26261  aannenlem2  26270  aaliou2  26281  tayl0  26302  dvtaylp  26311  taylthlem1  26314  taylthlem2  26315  taylthlem2OLD  26316  pserdvlem2  26371  logbcl  26710  relogbreexp  26718  relogbcxp  26728  cxplogb  26729  dcubic  26789  rlimcnp  26908  jensen  26932  dmgmaddn0  26966  dmlogdmgm  26967  lgamgulmlem2  26973  igamz  26991  gamp1  27001  regamcl  27004  wilthlem2  27012  basellem3  27026  chpub  27164  logexprlim  27169  lgslem1  27241  lgslem4  27244  lgsvalmod  27260  lgsqr  27295  lgsqrmod  27296  lgsqrmodndvds  27297  gausslemma2dlem0b  27301  gausslemma2dlem0c  27302  gausslemma2dlem0i  27308  gausslemma2dlem1a  27309  gausslemma2dlem4  27313  gausslemma2dlem5a  27314  gausslemma2dlem7  27317  gausslemma2d  27318  lgsquad2  27330  m1lgs  27332  2lgsoddprm  27360  2sqreultblem  27392  dchrisum0fno1  27455  rplogsum  27471  ishpg  28739  elntg2  28965  umgrislfupgrlem  29102  usgruspgrb  29163  nbumgrvtx  29326  nbupgrres  29344  isuvtx  29375  cusgrexilem2  29422  cusgrexi  29423  structtocusgr  29426  cusgrres  29429  cusgrfilem2  29437  vtxdginducedm1  29524  cusconngr  30170  2pthfrgr  30263  frgrncvvdeq  30288  frgrwopreglem4  30294  frgrwopreglem5  30300  frgrwopreg  30302  frgrhash2wsp  30311  strlem1  32229  strlem3  32232  strlem4  32233  strlem5  32234  hstrlem3  32240  hstrlem4  32241  iundisjf  32568  suppss3  32697  iundisjfi  32769  suppssnn0  32780  ind0  32831  qsdrngi  33459  zringidom  33515  zringfrac  33518  irngnzply1  33679  qtophaus  33819  elzdif0  33963  measvunilem  34195  sibfof  34324  eulerpartlemb  34352  eulerpartlemf  34354  sseqf  34376  ballotlem5  34484  ballotlemi1  34487  ballotlemii  34488  ballotlemic  34491  ballotlem1c  34492  ballotlemscr  34503  ballotlemro  34507  ballotlemfg  34510  ballotlemfrc  34511  ballotlemfrceq  34513  ballotlemrinv0  34517  plymulx0  34531  signstfvn  34553  signsvfn  34566  bnj923  34751  bnj570  34888  bnj594  34895  subfacp1lem1  35159  satffunlem2lem1  35384  mrsubcn  35499  mrsubco  35501  circum  35654  dfon2lem6  35769  neibastop1  36340  bj-restn0b  37072  lindsadd  37600  lindsenlbs  37602  matunitlindflem1  37603  poimirlem24  37631  poimirlem25  37632  dvtan  37657  itg2addnclem2  37659  ftc1cnnc  37679  dvasin  37691  dvreasin  37693  dvreacos  37694  isdrngo2  37945  isdrngo3  37946  divrngidl  38015  isfldidl  38055  pridlc2  38059  pridlc3  38060  prter2  38867  lsateln0  38981  lsatlss  38982  lsmsat  38994  lsatcv0  39017  lsat0cv  39019  lcv1  39027  l1cvpat  39040  dih1dimatlem  41316  dihatexv2  41326  djhcvat42  41402  dihjat1lem  41415  dochsatshp  41438  lcfl6  41487  mapdrvallem2  41632  mapdpglem32  41692  idomnnzgmulnz  42114  aks6d1c5lem3  42118  aks6d1c5lem2  42119  deg1gprod  42121  sticksstones22  42149  unitscyglem4  42179  readvrec2  42342  readvrec  42343  readvcot  42345  evlsvvvallem  42542  evlsvvvallem2  42543  evlsvvval  42544  evlsbagval  42547  selvvvval  42566  evlselv  42568  evlsmhpvvval  42576  prjspertr  42586  prjsperref  42587  prjspersym  42588  prjspvs  42591  prjsprellsp  42592  dffltz  42615  irrapx1  42809  pell1234qrne0  42834  pell1234qrreccl  42835  pell1234qrmulcl  42836  pell14qrgt0  42840  pell1234qrdich  42842  pell14qrdich  42850  pell1qrge1  42851  pell1qr1  42852  pell1qrgap  42855  pell14qrgapw  42857  pellqrexplicit  42858  pellqrex  42860  pellfundge  42863  pellfundgt1  42864  setindtr  43006  kelac1  43045  mpaaeu  43132  flcidc  43152  deg1mhm  43182  onexoegt  43226  cantnfub  43303  cantnfresb  43306  succlg  43310  dflim5  43311  onmcl  43313  omabs2  43314  tfsconcatrev  43330  minregex2  43517  radcnvrat  44296  binomcxplemdvbinom  44335  disjiun2  45045  fiiuncl  45052  disjf1o  45178  difmapsn  45199  supminfxr2  45458  icoiccdif  45515  iccdificc  45530  fsumnncl  45563  fsumsupp0  45569  fprod0  45587  climrec  45594  islpcn  45630  lptre2pt  45631  limclner  45642  cnrefiisplem  45820  fprodcncf  45891  fperdvper  45910  dvdivcncf  45918  dvnmul  45934  dvmptfprodlem  45935  dvnprodlem2  45938  stoweidlem25  46016  stoweidlem28  46019  stoweidlem41  46032  stoweidlem44  46035  stoweidlem46  46037  stirlinglem5  46069  dirkercncflem1  46094  dirkercncflem2  46095  fourierdlem24  46122  fourierdlem62  46159  fouriersw  46222  fouriercn  46223  elaa2lem  46224  elaa2  46225  etransclem25  46250  etransclem35  46260  etransclem44  46269  sge0iunmptlemfi  46404  sge0fodjrnlem  46407  iundjiunlem  46450  meadjiunlem  46456  meaiininclem  46477  isomenndlem  46521  hsphoidmvle2  46576  hsphoidmvle  46577  hoidmv1lelem2  46583  hoidmvle  46591  ovnhoilem1  46592  hspdifhsp  46607  hspmbllem2  46618  ovnsubadd2lem  46636  ovolval4lem1  46640  preimagelt  46690  preimalegt  46691  fsummsndifre  47366  fsummmodsndifre  47368  odz2prm2pw  47557  fmtnoprmfac1lem  47558  fmtnoprmfac2lem1  47560  2pwp1prm  47583  lighneallem2  47600  lighneallem3  47601  lighneallem4  47604  bgoldbtbndlem2  47800  bgoldbtbndlem3  47801  bgoldbtbndlem4  47802  bgoldbtbnd  47803  isubgrvtxuhgr  47857  2zrngnmlid2  48238  mgpsumunsn  48342  mgpsumz  48343  mgpsumn  48344  lindslinindsimp1  48439  lindslinindsimp2  48445  lincresunit1  48459  lincresunit2  48460  lincresunit3lem1  48461  lincresunit3lem2  48462  lincresunit3  48463  lindssnlvec  48468  logcxp0  48517  relogbmulbexp  48543  relogbdivb  48544  dignn0fr  48583  rrxlinesc  48717  eenglngeehlnmlem1  48719  eenglngeehlnmlem2  48720