Theorem eldifi 4091

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 501	1 ⊢ (𝐴 ∈ (𝐵 ∖ 𝐶) → 𝐴 ∈ 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3463  df-dif 3914

This theorem is referenced by:  difss  4096  eqoreldif  4654  xpdifid  6166  xpdifcnvepel  6167  tz7.7  6387  tfi  7849  peano5  7890  resf1extb  7931  resf1ext2b  7932  xpord2pred  8141  frrlem12  8294  frrlem13  8295  tz7.48-1  8430  tz7.49  8432  dif20el  8490  oaf1o  8548  oeordi  8573  oeord  8574  oecan  8575  oeword  8576  oeworde  8579  oelimcl  8586  oeeulem  8587  oeeui  8588  oaabs2  8635  boxcutc  8939  domdifsn  9048  pssnn  9153  isinf  9225  pwfilem  9277  fsuppco2  9363  fsuppcor  9364  ordtypelem7  9486  unxpwdom2  9550  inf3lem3  9599  cantnfp1lem1  9647  cantnfp1lem3  9649  ttrcltr  9685  infxpenc2lem1  10003  dfacacn  10125  isf32lem3  10339  isf34lem4  10361  fin67  10379  isfin7-2  10380  domtriomlem  10426  axdc2lem  10432  axdc3lem4  10437  axdc4lem  10439  ttukeylem7  10499  konigthlem  10553  fpwwe2lem12  10627  fpwwe2  10628  ind0  12228  modfzo0difsn  13979  hashf1lem1  14492  hashle2prv  14515  rlimrege0  15630  rlimrecl  15631  sumrblem  15762  fsumcvg  15763  summolem2a  15766  fsumss  15776  fsumsplit1  15796  fsumless  15848  cvgcmpce  15870  binomlem  15883  incexclem  15890  incexc  15891  isumltss  15902  prodrblem  15983  fprodcvg  15984  prodmolem2a  15988  fprodss  16002  fprodn0f  16045  fprodeq0g  16048  fprodmodd  16051  rpnnen2lem10  16279  rpnnen2lem11  16280  sumeven  16445  sumodd  16446  lcmfunsnlem2  16698  oddprmge3  16759  oddprm  16870  nnoddn2prm  16871  nnoddn2prmb  16873  iserodd  16895  prmreclem2  16977  prmreclem3  16978  prmreclem5  16980  4sqlem19  17023  prmdvdsprmo  17102  prmodvdslcmf  17107  prmlem0  17165  firest  17485  chnccat  18682  chnrev  18683  grpinvnzcl  19077  symgextfv  19488  pmtrf  19525  pmtrdifellem3  19548  sylow2alem2  19688  sylow2a  19689  efgsf  19799  efgsrel  19804  efgs1  19805  efgsfo  19809  gsumzaddlem  19991  gsumzadd  19992  gsumzmhm  20007  gsum2d2lem  20043  dprdfadd  20092  dprdres  20100  subgdmdprd  20106  dmdprdsplitlem  20109  dmdprdsplit2lem  20117  dpjidcl  20130  ablfac1b  20142  pgpfac1lem1  20146  gsummgp0  20399  isirred  20501  irredrmul  20509  ringelnzr  20607  c0rhm  20619  c0rnghm  20620  zrrnghm  20621  zrinitorngc  20727  zrtermorngc  20728  isdomn2  20796  isdomn4  20800  isdrng2  20827  drngmcl  20834  isdrngd  20847  isdrngdOLD  20849  imadrhmcl  20878  cntzsdrg  20883  lcomfsupp  21001  lbspropd  21198  lspsneq  21224  lsppratlem6  21254  lbsextlem2  21261  lbsextlem4  21263  cnsubrg  21546  xrs1mnd  21559  xrs10  21560  xrs1cmn  21561  psgnodpm  21707  zrhpsgnodpm  21711  evpmodpmf1o  21715  uvcresum  21912  frlmssuvc1  21913  frlmsslsp  21915  frlmup2  21918  lindfrn  21940  f1lindf  21941  lindfmm  21946  islindf4  21957  psrbaglesupp  22041  psrlidm  22080  psrridm  22081  mplsubglem  22117  mpllsslem  22118  mplsubrglem  22122  mplmonmul  22156  mplcoe1  22157  mplcoe5  22160  mplbas2  22162  evlslem3  22200  evlsvvvallem  22211  evlsvvvallem2  22212  evlsvvval  22213  selvvvval  22262  mhpvscacl  22286  psdmul  22298  coe1tmmul2  22406  coe1tmmul  22407  dmatmul  22623  1marepvsma1  22709  mdetdiaglem  22724  mdetrlin  22728  mdetrsca  22729  mdetralt  22734  maducoeval2  22766  madugsum  22769  symgmatr01  22780  gsummatr01lem3  22783  gsummatr01lem4  22784  gsummatr01  22785  smadiadetlem0  22787  smadiadetlem1a  22789  cmpfi  23534  2ndcdisj2  23583  elptr2  23700  ptcnplem  23747  xkopt  23781  kqdisj  23858  fin1aufil  24058  ptcmplem2  24179  ptcmplem3  24180  ptcmplem4  24181  opnsubg  24234  lpbl  24629  blcld  24631  zcld  24940  recld2  24941  reconnlem1  24953  divcn  24996  iundisj  25676  mbfeqalem1  25769  itg1val2  25812  itg1ge0  25814  i1fmullem  25822  i1fadd  25823  itg1addlem4  25827  itg1mulc  25832  itg1lea  25840  itg1le  25841  mbfi1fseqlem4  25846  itg2uba  25871  itg2lea  25872  itg2eqa  25873  itg2splitlem  25876  itg2split  25877  itgeqa  25942  ellimc3  26007  dvaddbr  26066  dvmulbr  26067  dvcobr  26074  dvcjbr  26077  dvrec  26083  dvrecg  26101  dvcnvlem  26104  dvexp3  26106  dveflem  26107  tdeglem4  26186  deg1n0ima  26215  deg1mul3le  26243  ig1peu  26301  ply1termlem  26329  plypf1  26338  plyaddlem1  26339  plymullem1  26340  coeeulem  26350  coeidlem  26363  coeid3  26366  coefv0  26374  coemulhi  26380  coemulc  26381  plyn0mulidp  26411  dvply1  26414  fta1  26438  vieta1lem2  26441  elaa  26446  elqaalem2  26450  aannenlem2  26459  aaliou2  26470  tayl0  26491  dvtaylp  26499  taylthlem1  26502  taylthlem2  26503  pserdvlem2  26557  logbcl  26898  relogbreexp  26906  relogbcxp  26916  cxplogb  26917  dcubic  26977  rlimcnp  27096  jensen  27119  dmgmaddn0  27153  dmlogdmgm  27154  lgamgulmlem2  27160  igamz  27178  gamp1  27188  regamcl  27191  wilthlem2  27199  basellem3  27213  chpub  27350  logexprlim  27355  lgslem1  27427  lgslem4  27430  lgsvalmod  27446  lgsqr  27481  lgsqrmod  27482  lgsqrmodndvds  27483  gausslemma2dlem0b  27487  gausslemma2dlem0c  27488  gausslemma2dlem0i  27494  gausslemma2dlem1a  27495  gausslemma2dlem4  27499  gausslemma2dlem5a  27500  gausslemma2dlem7  27503  gausslemma2d  27504  lgsquad2  27516  m1lgs  27518  2lgsoddprm  27546  2sqreultblem  27578  dchrisum0fno1  27641  rplogsum  27657  ishpg  29000  elntg2  29276  umgrislfupgrlem  29413  usgruspgrb  29474  nbumgrvtx  29637  nbupgrres  29655  isuvtx  29686  cusgrexilem2  29733  cusgrexi  29734  structtocusgr  29737  cusgrres  29739  cusgrfilem2  29747  vtxdginducedm1  29834  cusconngr  30483  2pthfrgr  30576  frgrncvvdeq  30601  frgrwopreglem4  30607  frgrwopreglem5  30613  frgrwopreg  30615  frgrhash2wsp  30624  strlem1  32543  strlem3  32546  strlem4  32547  strlem5  32548  hstrlem3  32554  hstrlem4  32555  iundisjf  32875  suppss3  33009  iundisjfi  33082  suppssnn0  33091  qsdrngi  33722  zringidom  33786  zringfrac  33789  psrmonmul  33885  irngnzply1  34026  qtophaus  34171  elzdif0  34315  measvunilem  34547  sibfof  34675  eulerpartlemb  34703  eulerpartlemf  34705  sseqf  34727  ballotlem5  34835  ballotlemi1  34838  ballotlemii  34839  ballotlemic  34842  ballotlem1c  34843  ballotlemscr  34854  ballotlemro  34858  ballotlemfg  34861  ballotlemfrc  34862  ballotlemfrceq  34864  ballotlemrinv0  34868  signstfvn  34901  signsvfn  34914  bnj923  35102  bnj570  35238  bnj594  35245  fineqvnttrclselem1  35467  fineqvnttrclselem2  35468  fineqvnttrclselem3  35469  fineqvnttrclse  35470  subfacp1lem1  35604  satffunlem2lem1  35829  mrsubcn  35944  mrsubco  35946  circum  36099  dfon2lem6  36211  neibastop1  36793  bj-restn0b  37656  lindsadd  38187  lindsenlbs  38189  matunitlindflem1  38190  poimirlem24  38218  poimirlem25  38219  dvtan  38244  itg2addnclem2  38246  ftc1cnnc  38266  dvasin  38278  dvreasin  38280  dvreacos  38281  isdrngo2  38532  isdrngo3  38533  divrngidl  38602  isfldidl  38642  pridlc2  38646  pridlc3  38647  blockadjliftmap  39032  prter2  39580  lsateln0  39694  lsatlss  39695  lsmsat  39707  lsatcv0  39730  lsat0cv  39732  lcv1  39740  l1cvpat  39753  dih1dimatlem  42028  dihatexv2  42038  djhcvat42  42114  dihjat1lem  42127  dochsatshp  42150  lcfl6  42199  mapdrvallem2  42344  mapdpglem32  42404  idomnnzgmulnz  42825  aks6d1c5lem3  42829  aks6d1c5lem2  42830  deg1gprod  42832  sticksstones22  42860  unitscyglem4  42890  readvrec2  43047  readvrec  43048  readvcot  43050  evlsbagval  43245  evlselv  43248  evlsmhpvvval  43254  prjspertr  43264  prjsperref  43265  prjspersym  43266  prjspvs  43269  prjsprellsp  43270  dffltz  43293  irrapx1  43482  pell1234qrne0  43507  pell1234qrreccl  43508  pell1234qrmulcl  43509  pell14qrgt0  43513  pell1234qrdich  43515  pell14qrdich  43523  pell1qrge1  43524  pell1qr1  43525  pell1qrgap  43528  pell14qrgapw  43530  pellqrexplicit  43531  pellqrex  43533  pellfundge  43536  pellfundgt1  43537  setindtr  43678  kelac1  43717  mpaaeu  43804  flcidc  43824  deg1mhm  43854  onexoegt  43898  cantnfub  43975  cantnfresb  43978  succlg  43982  dflim5  43983  onmcl  43985  omabs2  43986  tfsconcatrev  44002  minregex2  44188  radcnvrat  44951  binomcxplemdvbinom  44990  disjiun2  45705  fiiuncl  45712  disjf1o  45836  difmapsn  45855  supminfxr2  46110  icoiccdif  46167  iccdificc  46182  fsumnncl  46215  fsumsupp0  46221  fprod0  46239  climrec  46246  islpcn  46280  lptre2pt  46281  limclner  46292  cnrefiisplem  46470  fprodcncf  46541  fperdvper  46560  dvdivcncf  46568  dvnmul  46584  dvmptfprodlem  46585  dvnprodlem2  46588  stoweidlem25  46666  stoweidlem28  46669  stoweidlem41  46682  stoweidlem44  46685  stoweidlem46  46687  stirlinglem5  46719  dirkercncflem1  46744  dirkercncflem2  46745  fourierdlem24  46772  fourierdlem62  46809  fouriersw  46872  fouriercn  46873  elaa2lem  46874  elaa2  46875  etransclem25  46900  etransclem35  46910  etransclem44  46919  sge0iunmptlemfi  47054  sge0fodjrnlem  47057  iundjiunlem  47100  meadjiunlem  47106  meaiininclem  47127  isomenndlem  47171  hsphoidmvle2  47226  hsphoidmvle  47227  hoidmv1lelem2  47233  hoidmvle  47241  ovnhoilem1  47242  hspdifhsp  47257  hspmbllem2  47268  ovnsubadd2lem  47286  ovolval4lem1  47290  preimagelt  47340  preimalegt  47341  chnsubseq  47523  fsummsndifre  48041  fsummmodsndifre  48043  odz2prm2pw  48239  fmtnoprmfac1lem  48240  fmtnoprmfac2lem1  48242  2pwp1prm  48265  lighneallem2  48282  lighneallem3  48283  lighneallem4  48286  bgoldbtbndlem2  48495  bgoldbtbndlem3  48496  bgoldbtbndlem4  48497  bgoldbtbnd  48498  isubgrvtxuhgr  48553  2zrngnmlid2  48946  mgpsumunsn  49061  mgpsumz  49062  mgpsumn  49063  lindslinindsimp1  49157  lindslinindsimp2  49163  lincresunit1  49177  lincresunit2  49178  lincresunit3lem1  49179  lincresunit3lem2  49180  lincresunit3  49181  lindssnlvec  49186  logcxp0  49235  relogbmulbexp  49261  relogbdivb  49262  dignn0fr  49301  rrxlinesc  49435  eenglngeehlnmlem1  49437  eenglngeehlnmlem2  49438