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  9561  cantnfp1lem1  9609  cantnfp1lem3  9611  ttrcltr  9647  infxpenc2lem1  9950  dfacacn  10073  isf32lem3  10286  isf34lem4  10308  fin67  10326  isfin7-2  10327  domtriomlem  10373  axdc2lem  10379  axdc3lem4  10384  axdc4lem  10386  ttukeylem7  10446  konigthlem  10499  fpwwe2lem12  10573  fpwwe2  10574  modfzo0difsn  13886  hashf1lem1  14398  hashle2prv  14421  rlimrege0  15522  rlimrecl  15523  sumrblem  15654  fsumcvg  15655  summolem2a  15658  fsumss  15668  fsumsplit1  15688  fsumless  15739  cvgcmpce  15761  binomlem  15772  incexclem  15779  incexc  15780  isumltss  15791  prodrblem  15872  fprodcvg  15873  prodmolem2a  15877  fprodss  15891  fprodn0f  15934  fprodeq0g  15937  fprodmodd  15940  rpnnen2lem10  16168  rpnnen2lem11  16169  sumeven  16334  sumodd  16335  lcmfunsnlem2  16587  oddprmge3  16647  oddprm  16758  nnoddn2prm  16759  nnoddn2prmb  16761  iserodd  16783  prmreclem2  16865  prmreclem3  16866  prmreclem5  16868  4sqlem19  16911  prmdvdsprmo  16990  prmodvdslcmf  16995  prmlem0  17053  firest  17372  grpinvnzcl  18926  symgextfv  19333  pmtrf  19370  pmtrdifellem3  19393  sylow2alem2  19533  sylow2a  19534  efgsf  19644  efgsrel  19649  efgs1  19650  efgsfo  19654  gsumzaddlem  19836  gsumzadd  19837  gsumzmhm  19852  gsum2d2lem  19888  dprdfadd  19937  dprdres  19945  subgdmdprd  19951  dmdprdsplitlem  19954  dmdprdsplit2lem  19962  dpjidcl  19975  ablfac1b  19987  pgpfac1lem1  19991  gsummgp0  20239  isirred  20340  irredrmul  20348  ringelnzr  20444  c0rhm  20455  c0rnghm  20456  zrrnghm  20457  zrinitorngc  20563  zrtermorngc  20564  isdomn2  20632  isdomn4  20637  isdrng2  20664  drngmcl  20671  isdrngd  20686  isdrngdOLD  20688  imadrhmcl  20718  cntzsdrg  20723  lcomfsupp  20841  lbspropd  21039  lspsneq  21065  lsppratlem6  21095  lbsextlem2  21102  lbsextlem4  21104  cnsubrg  21370  xrs1mnd  21383  xrs10  21384  xrs1cmn  21385  psgnodpm  21531  zrhpsgnodpm  21535  evpmodpmf1o  21539  uvcresum  21736  frlmssuvc1  21737  frlmsslsp  21739  frlmup2  21742  lindfrn  21764  f1lindf  21765  lindfmm  21770  islindf4  21781  psrbaglesupp  21865  psrlidm  21905  psrridm  21906  mplsubglem  21942  mpllsslem  21943  mplsubrglem  21947  mplmonmul  21977  mplcoe1  21978  mplcoe5  21981  mplbas2  21983  evlslem3  22021  mhpvscacl  22075  psdmul  22087  coe1tmmul2  22196  coe1tmmul  22197  dmatmul  22418  1marepvsma1  22504  mdetdiaglem  22519  mdetrlin  22523  mdetrsca  22524  mdetralt  22529  maducoeval2  22561  madugsum  22564  symgmatr01  22575  gsummatr01lem3  22578  gsummatr01lem4  22579  gsummatr01  22580  smadiadetlem0  22582  smadiadetlem1a  22584  cmpfi  23329  2ndcdisj2  23378  elptr2  23495  ptcnplem  23542  xkopt  23576  kqdisj  23653  fin1aufil  23853  ptcmplem2  23974  ptcmplem3  23975  ptcmplem4  23976  opnsubg  24029  lpbl  24425  blcld  24427  zcld  24736  recld2  24737  reconnlem1  24749  divcnOLD  24791  divcn  24793  iundisj  25483  mbfeqalem1  25576  itg1val2  25619  itg1ge0  25621  i1fmullem  25629  i1fadd  25630  itg1addlem4  25634  itg1mulc  25639  itg1lea  25647  itg1le  25648  mbfi1fseqlem4  25653  itg2uba  25678  itg2lea  25679  itg2eqa  25680  itg2splitlem  25683  itg2split  25684  itgeqa  25749  ellimc3  25814  dvaddbr  25874  dvmulbr  25875  dvmulbrOLD  25876  dvcobr  25883  dvcobrOLD  25884  dvcjbr  25887  dvrec  25893  dvrecg  25911  dvcnvlem  25914  dvexp3  25916  dveflem  25917  tdeglem4  25999  deg1n0ima  26028  deg1mul3le  26056  ig1peu  26114  ply1termlem  26142  plypf1  26151  plyaddlem1  26152  plymullem1  26153  coeeulem  26163  coeidlem  26176  coeid3  26179  coefv0  26187  coemulhi  26193  coemulc  26194  dvply1  26225  fta1  26250  vieta1lem2  26253  elaa  26258  elqaalem2  26262  aannenlem2  26271  aaliou2  26282  tayl0  26303  dvtaylp  26312  taylthlem1  26315  taylthlem2  26316  taylthlem2OLD  26317  pserdvlem2  26372  logbcl  26711  relogbreexp  26719  relogbcxp  26729  cxplogb  26730  dcubic  26790  rlimcnp  26909  jensen  26933  dmgmaddn0  26967  dmlogdmgm  26968  lgamgulmlem2  26974  igamz  26992  gamp1  27002  regamcl  27005  wilthlem2  27013  basellem3  27027  chpub  27165  logexprlim  27170  lgslem1  27242  lgslem4  27245  lgsvalmod  27261  lgsqr  27296  lgsqrmod  27297  lgsqrmodndvds  27298  gausslemma2dlem0b  27302  gausslemma2dlem0c  27303  gausslemma2dlem0i  27309  gausslemma2dlem1a  27310  gausslemma2dlem4  27314  gausslemma2dlem5a  27315  gausslemma2dlem7  27318  gausslemma2d  27319  lgsquad2  27331  m1lgs  27333  2lgsoddprm  27361  2sqreultblem  27393  dchrisum0fno1  27456  rplogsum  27472  ishpg  28740  elntg2  28966  umgrislfupgrlem  29103  usgruspgrb  29164  nbumgrvtx  29327  nbupgrres  29345  isuvtx  29376  cusgrexilem2  29423  cusgrexi  29424  structtocusgr  29427  cusgrres  29430  cusgrfilem2  29438  vtxdginducedm1  29525  cusconngr  30171  2pthfrgr  30264  frgrncvvdeq  30289  frgrwopreglem4  30295  frgrwopreglem5  30301  frgrwopreg  30303  frgrhash2wsp  30312  strlem1  32230  strlem3  32233  strlem4  32234  strlem5  32235  hstrlem3  32241  hstrlem4  32242  iundisjf  32569  suppss3  32698  iundisjfi  32770  suppssnn0  32781  ind0  32832  qsdrngi  33460  zringidom  33516  zringfrac  33519  irngnzply1  33680  qtophaus  33820  elzdif0  33964  measvunilem  34196  sibfof  34325  eulerpartlemb  34353  eulerpartlemf  34355  sseqf  34377  ballotlem5  34485  ballotlemi1  34488  ballotlemii  34489  ballotlemic  34492  ballotlem1c  34493  ballotlemscr  34504  ballotlemro  34508  ballotlemfg  34511  ballotlemfrc  34512  ballotlemfrceq  34514  ballotlemrinv0  34518  plymulx0  34532  signstfvn  34554  signsvfn  34567  bnj923  34752  bnj570  34889  bnj594  34896  subfacp1lem1  35160  satffunlem2lem1  35385  mrsubcn  35500  mrsubco  35502  circum  35655  dfon2lem6  35770  neibastop1  36341  bj-restn0b  37073  lindsadd  37601  lindsenlbs  37603  matunitlindflem1  37604  poimirlem24  37632  poimirlem25  37633  dvtan  37658  itg2addnclem2  37660  ftc1cnnc  37680  dvasin  37692  dvreasin  37694  dvreacos  37695  isdrngo2  37946  isdrngo3  37947  divrngidl  38016  isfldidl  38056  pridlc2  38060  pridlc3  38061  prter2  38868  lsateln0  38982  lsatlss  38983  lsmsat  38995  lsatcv0  39018  lsat0cv  39020  lcv1  39028  l1cvpat  39041  dih1dimatlem  41317  dihatexv2  41327  djhcvat42  41403  dihjat1lem  41416  dochsatshp  41439  lcfl6  41488  mapdrvallem2  41633  mapdpglem32  41693  idomnnzgmulnz  42115  aks6d1c5lem3  42119  aks6d1c5lem2  42120  deg1gprod  42122  sticksstones22  42150  unitscyglem4  42180  readvrec2  42343  readvrec  42344  readvcot  42346  evlsvvvallem  42543  evlsvvvallem2  42544  evlsvvval  42545  evlsbagval  42548  selvvvval  42567  evlselv  42569  evlsmhpvvval  42577  prjspertr  42587  prjsperref  42588  prjspersym  42589  prjspvs  42592  prjsprellsp  42593  dffltz  42616  irrapx1  42810  pell1234qrne0  42835  pell1234qrreccl  42836  pell1234qrmulcl  42837  pell14qrgt0  42841  pell1234qrdich  42843  pell14qrdich  42851  pell1qrge1  42852  pell1qr1  42853  pell1qrgap  42856  pell14qrgapw  42858  pellqrexplicit  42859  pellqrex  42861  pellfundge  42864  pellfundgt1  42865  setindtr  43007  kelac1  43046  mpaaeu  43133  flcidc  43153  deg1mhm  43183  onexoegt  43227  cantnfub  43304  cantnfresb  43307  succlg  43311  dflim5  43312  onmcl  43314  omabs2  43315  tfsconcatrev  43331  minregex2  43518  radcnvrat  44297  binomcxplemdvbinom  44336  disjiun2  45046  fiiuncl  45053  disjf1o  45179  difmapsn  45200  supminfxr2  45459  icoiccdif  45516  iccdificc  45531  fsumnncl  45564  fsumsupp0  45570  fprod0  45588  climrec  45595  islpcn  45631  lptre2pt  45632  limclner  45643  cnrefiisplem  45821  fprodcncf  45892  fperdvper  45911  dvdivcncf  45919  dvnmul  45935  dvmptfprodlem  45936  dvnprodlem2  45939  stoweidlem25  46017  stoweidlem28  46020  stoweidlem41  46033  stoweidlem44  46036  stoweidlem46  46038  stirlinglem5  46070  dirkercncflem1  46095  dirkercncflem2  46096  fourierdlem24  46123  fourierdlem62  46160  fouriersw  46223  fouriercn  46224  elaa2lem  46225  elaa2  46226  etransclem25  46251  etransclem35  46261  etransclem44  46270  sge0iunmptlemfi  46405  sge0fodjrnlem  46408  iundjiunlem  46451  meadjiunlem  46457  meaiininclem  46478  isomenndlem  46522  hsphoidmvle2  46577  hsphoidmvle  46578  hoidmv1lelem2  46584  hoidmvle  46592  ovnhoilem1  46593  hspdifhsp  46608  hspmbllem2  46619  ovnsubadd2lem  46637  ovolval4lem1  46641  preimagelt  46691  preimalegt  46692  fsummsndifre  47367  fsummmodsndifre  47369  odz2prm2pw  47558  fmtnoprmfac1lem  47559  fmtnoprmfac2lem1  47561  2pwp1prm  47584  lighneallem2  47601  lighneallem3  47602  lighneallem4  47605  bgoldbtbndlem2  47801  bgoldbtbndlem3  47802  bgoldbtbndlem4  47803  bgoldbtbnd  47804  isubgrvtxuhgr  47858  2zrngnmlid2  48239  mgpsumunsn  48343  mgpsumz  48344  mgpsumn  48345  lindslinindsimp1  48440  lindslinindsimp2  48446  lincresunit1  48460  lincresunit2  48461  lincresunit3lem1  48462  lincresunit3lem2  48463  lincresunit3  48464  lindssnlvec  48469  logcxp0  48518  relogbmulbexp  48544  relogbdivb  48545  dignn0fr  48584  rrxlinesc  48718  eenglngeehlnmlem1  48720  eenglngeehlnmlem2  48721