Theorem eldifi 3989

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2048   ∖ cdif 3822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-dif 3828

This theorem is referenced by:  difss  3994  noelOLD  4179  eqoreldif  4490  xpdifid  5859  tz7.7  6049  tfi  7378  peano5  7414  wfrlem10  7761  wfrlem15  7766  tz7.48-1  7875  tz7.49  7877  dif20el  7924  oaf1o  7982  oeordi  8006  oeord  8007  oecan  8008  oeword  8009  oeworde  8012  oelimcl  8019  oeeulem  8020  oeeui  8021  oaabs2  8064  boxcutc  8294  domdifsn  8388  isinf  8518  pssnn  8523  pwfilem  8605  fsuppco2  8653  fsuppcor  8654  ordtypelem7  8775  unxpwdom2  8839  inf3lem3  8879  cantnfp1lem1  8927  cantnfp1lem3  8929  infxpenc2lem1  9231  dfacacn  9353  isf32lem3  9567  isf34lem4  9589  fin67  9607  isfin7-2  9608  domtriomlem  9654  axdc2lem  9660  axdc3lem4  9665  axdc4lem  9667  ttukeylem7  9727  konigthlem  9780  fpwwe2lem13  9854  fpwwe2  9855  modfzo0difsn  13119  hashf1lem1  13616  hashle2prv  13637  rlimrege0  14787  rlimrecl  14788  sumrblem  14918  fsumcvg  14919  summolem2a  14922  fsumss  14932  fsumless  15001  cvgcmpce  15023  binomlem  15034  incexclem  15041  incexc  15042  isumltss  15053  prodrblem  15133  fprodcvg  15134  prodmolem2a  15138  fprodss  15152  fprodn0f  15195  fprodeq0g  15198  fprodmodd  15201  rpnnen2lem10  15426  rpnnen2lem11  15427  sumeven  15588  sumodd  15589  lcmfunsnlem2  15830  oddprmge3  15890  oddprm  15993  nnoddn2prm  15994  nnoddn2prmb  15996  iserodd  16018  prmreclem2  16099  prmreclem3  16100  prmreclem5  16102  4sqlem19  16145  prmdvdsprmo  16224  prmodvdslcmf  16229  prmlem0  16285  firest  16552  grpinvnzcl  17948  symgextfv  18297  pmtrf  18334  pmtrdifellem3  18357  sylow2alem2  18494  sylow2a  18495  efgsf  18603  efgsrel  18608  efgs1  18609  efgsfo  18614  efgredlemc  18620  gsumzaddlem  18784  gsumzadd  18785  gsumzmhm  18800  gsum2d2lem  18836  dprdfadd  18882  dprdres  18890  subgdmdprd  18896  dmdprdsplitlem  18899  dmdprdsplit2lem  18907  dpjidcl  18920  ablfac1b  18932  pgpfac1lem1  18936  gsummgp0  19071  isirred  19162  irredrmul  19170  isdrng2  19225  isdrngd  19240  cntzsdrg  19293  lcomfsupp  19386  lbspropd  19583  lspsneq  19606  lsppratlem6  19636  lbsextlem2  19643  lbsextlem4  19645  ringelnzr  19750  psrbaglesupp  19852  psrlidm  19887  psrridm  19888  mplsubglem  19918  mpllsslem  19919  mplsubrglem  19923  mplmonmul  19948  mplcoe1  19949  mplcoe5  19952  mplbas2  19954  evlslem3  19997  coe1tmmul2  20137  coe1tmmul  20138  xrs1mnd  20275  xrs10  20276  xrs1cmn  20277  cnsubrg  20297  psgnodpm  20424  zrhpsgnodpm  20428  evpmodpmf1o  20432  uvcresum  20629  frlmssuvc1  20630  frlmsslsp  20632  frlmup2  20635  lindfrn  20657  f1lindf  20658  lindfmm  20663  islindf4  20674  dmatmul  20800  1marepvsma1  20886  mdetdiaglem  20901  mdetrlin  20905  mdetrsca  20906  mdetralt  20911  maducoeval2  20943  madugsum  20946  symgmatr01  20957  gsummatr01lem3  20960  gsummatr01lem4  20961  gsummatr01  20962  smadiadetlem0  20964  smadiadetlem1a  20966  cmpfi  21710  2ndcdisj2  21759  elptr2  21876  ptcnplem  21923  xkopt  21957  kqdisj  22034  fin1aufil  22234  ptcmplem2  22355  ptcmplem3  22356  ptcmplem4  22357  opnsubg  22409  lpbl  22806  blcld  22808  zcld  23114  recld2  23115  reconnlem1  23127  divcn  23169  iundisj  23842  mbfeqalem1  23935  itg1val2  23978  itg1ge0  23980  i1fmullem  23988  i1fadd  23989  itg1addlem4  23993  itg1mulc  23998  itg1lea  24006  itg1le  24007  mbfi1fseqlem4  24012  itg2uba  24037  itg2lea  24038  itg2eqa  24039  itg2splitlem  24042  itg2split  24043  itgeqa  24107  ellimc3  24170  dvaddbr  24228  dvmulbr  24229  dvcobr  24236  dvcjbr  24239  dvrec  24245  dvrecg  24263  dvcnvlem  24266  dvexp3  24268  dveflem  24269  tdeglem4  24347  deg1n0ima  24376  deg1mul3le  24403  ig1peu  24458  ply1termlem  24486  plypf1  24495  plyaddlem1  24496  plymullem1  24497  coeeulem  24507  coeidlem  24520  coeid3  24523  coefv0  24531  coemulhi  24537  coemulc  24538  dvply1  24566  fta1  24590  vieta1lem2  24593  elaa  24598  elqaalem2  24602  aannenlem2  24611  aaliou2  24622  tayl0  24643  dvtaylp  24651  taylthlem1  24654  taylthlem2  24655  pserdvlem2  24709  logbcl  25036  relogbreexp  25044  relogbcxp  25054  cxplogb  25055  dcubic  25115  rlimcnp  25235  jensen  25258  dmgmaddn0  25292  dmlogdmgm  25293  lgamgulmlem2  25299  igamz  25317  gamp1  25327  regamcl  25330  wilthlem2  25338  basellem3  25352  chpub  25488  logexprlim  25493  lgslem1  25565  lgslem4  25568  lgsvalmod  25584  lgsqr  25619  lgsqrmod  25620  lgsqrmodndvds  25621  gausslemma2dlem0b  25625  gausslemma2dlem0c  25626  gausslemma2dlem0i  25632  gausslemma2dlem1a  25633  gausslemma2dlem4  25637  gausslemma2dlem5a  25638  gausslemma2dlem7  25641  gausslemma2d  25642  lgsquad2  25654  m1lgs  25656  2lgsoddprm  25684  2sqreultblem  25716  dchrisum0fno1  25779  rplogsum  25795  ishpg  26237  elntg2  26464  umgrislfupgrlem  26600  usgruspgrb  26659  nbumgrvtx  26821  nbupgrres  26839  isuvtx  26870  cusgrexilem2  26917  cusgrexi  26918  structtocusgr  26921  cusgrres  26923  cusgrfilem2  26931  vtxdginducedm1  27018  cusconngr  27710  2pthfrgr  27808  frgrncvvdeq  27833  frgrwopreglem4  27839  frgrwopreglem5  27845  frgrwopreg  27847  frgrhash2wsp  27856  strlem1  29798  strlem3  29801  strlem4  29802  strlem5  29803  hstrlem3  29809  hstrlem4  29810  iundisjf  30095  suppss3  30201  iundisjfi  30257  qtophaus  30701  elzdif0  30822  ind0  30878  measvunilem  31073  sibfof  31200  eulerpartlemb  31228  eulerpartlemf  31230  sseqf  31253  ballotlem5  31360  ballotlemi1  31363  ballotlemii  31364  ballotlemic  31367  ballotlem1c  31368  ballotlemscr  31379  ballotlemro  31383  ballotlemfg  31386  ballotlemfrc  31387  ballotlemfrceq  31389  ballotlemrinv0  31393  plymulx0  31424  signstfvn  31446  bnj923  31648  bnj570  31785  bnj594  31792  subfacp1lem1  31971  mrsubcn  32226  mrsubco  32228  circum  32377  dfon2lem6  32493  frrlem12  32595  frrlem13  32596  neibastop1  33168  bj-restn0b  33827  lindsadd  34274  lindsenlbs  34276  matunitlindflem1  34277  poimirlem24  34305  poimirlem25  34306  dvtan  34331  itg2addnclem2  34333  ftc1cnnc  34355  dvasin  34367  dvreasin  34369  dvreacos  34370  isdrngo2  34626  isdrngo3  34627  divrngidl  34696  isfldidl  34736  pridlc2  34740  pridlc3  34741  prter2  35410  lsateln0  35524  lsatlss  35525  lsmsat  35537  lsatcv0  35560  lsat0cv  35562  lcv1  35570  l1cvpat  35583  dih1dimatlem  37858  dihatexv2  37868  djhcvat42  37944  dihjat1lem  37957  dochsatshp  37980  lcfl6  38029  mapdrvallem2  38174  mapdpglem32  38234  prjspertr  38607  prjsperref  38608  prjspersym  38609  prjspvs  38612  prjsprellsp  38613  dffltz  38623  irrapx1  38766  pell1234qrne0  38791  pell1234qrreccl  38792  pell1234qrmulcl  38793  pell14qrgt0  38797  pell1234qrdich  38799  pell14qrdich  38807  pell1qrge1  38808  pell1qr1  38809  pell1qrgap  38812  pell14qrgapw  38814  pellqrexplicit  38815  pellqrex  38817  pellfundge  38820  pellfundgt1  38821  setindtr  38962  kelac1  39004  mpaaeu  39091  flcidc  39115  deg1mhm  39148  radcnvrat  40006  binomcxplemdvbinom  40045  disjiun2  40684  fiiuncl  40691  disjf1o  40822  difmapsn  40846  supminfxr2  41122  icoiccdif  41177  iccdificc  41192  fsumnncl  41229  fsumsplit1  41230  fsumsupp0  41236  fprod0  41254  climrec  41261  islpcn  41297  lptre2pt  41298  limclner  41309  cnrefiisplem  41487  fprodcncf  41560  fperdvper  41579  dvdivcncf  41588  dvnmul  41604  dvmptfprodlem  41605  dvnprodlem2  41608  stoweidlem25  41687  stoweidlem28  41690  stoweidlem41  41703  stoweidlem44  41706  stoweidlem46  41708  stirlinglem5  41740  dirkercncflem1  41765  dirkercncflem2  41766  fourierdlem24  41793  fourierdlem62  41830  fouriersw  41893  fouriercn  41894  elaa2lem  41895  elaa2  41896  etransclem25  41921  etransclem35  41931  etransclem44  41940  sge0iunmptlemfi  42072  sge0fodjrnlem  42075  iundjiunlem  42118  meadjiunlem  42124  meaiininclem  42145  isomenndlem  42189  hsphoidmvle2  42244  hsphoidmvle  42245  hoidmv1lelem2  42251  hoidmvle  42259  ovnhoilem1  42260  hspdifhsp  42275  hspmbllem2  42286  ovnsubadd2lem  42304  ovolval4lem1  42308  preimagelt  42357  preimalegt  42358  fsummsndifre  42884  fsummmodsndifre  42886  odz2prm2pw  43033  fmtnoprmfac1lem  43034  fmtnoprmfac2lem1  43036  2pwp1prm  43059  lighneallem2  43079  lighneallem3  43080  lighneallem4  43083  bgoldbtbndlem2  43279  bgoldbtbndlem3  43280  bgoldbtbndlem4  43281  bgoldbtbnd  43282  c0rhm  43487  c0rnghm  43488  zrrnghm  43492  2zrngnmlid2  43526  zrinitorngc  43575  zrtermorngc  43576  mgpsumunsn  43713  mgpsumz  43714  mgpsumn  43715  lindslinindsimp1  43819  lindslinindsimp2  43825  lincresunit1  43839  lincresunit2  43840  lincresunit3lem1  43841  lincresunit3lem2  43842  lincresunit3  43843  lindssnlvec  43848  logcxp0  43903  relogbmulbexp  43929  relogbdivb  43930  dignn0fr  43969  rrxlinesc  44030  eenglngeehlnmlem1  44032  eenglngeehlnmlem2  44033