Theorem eldifi 4041

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2110   ∖ cdif 3863

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 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-dif 3869

This theorem is referenced by:  difss  4046  eqoreldif  4600  xpdifid  6031  tz7.7  6239  tfi  7632  peano5  7671  peano5OLD  7672  frrlem12  8038  frrlem13  8039  wfrlem10  8064  wfrlem15  8069  tz7.48-1  8179  tz7.49  8181  dif20el  8232  oaf1o  8291  oeordi  8315  oeord  8316  oecan  8317  oeword  8318  oeworde  8321  oelimcl  8328  oeeulem  8329  oeeui  8330  oaabs2  8374  boxcutc  8622  domdifsn  8728  pssnn  8846  pwfilem  8855  isinf  8891  pssnnOLD  8895  pwfilemOLD  8970  fsuppco2  9019  fsuppcor  9020  ordtypelem7  9140  unxpwdom2  9204  inf3lem3  9245  cantnfp1lem1  9293  cantnfp1lem3  9295  infxpenc2lem1  9633  dfacacn  9755  isf32lem3  9969  isf34lem4  9991  fin67  10009  isfin7-2  10010  domtriomlem  10056  axdc2lem  10062  axdc3lem4  10067  axdc4lem  10069  ttukeylem7  10129  konigthlem  10182  fpwwe2lem12  10256  fpwwe2  10257  modfzo0difsn  13516  hashf1lem1  14020  hashf1lem1OLD  14021  hashle2prv  14044  rlimrege0  15140  rlimrecl  15141  sumrblem  15275  fsumcvg  15276  summolem2a  15279  fsumss  15289  fsumsplit1  15309  fsumless  15360  cvgcmpce  15382  binomlem  15393  incexclem  15400  incexc  15401  isumltss  15412  prodrblem  15491  fprodcvg  15492  prodmolem2a  15496  fprodss  15510  fprodn0f  15553  fprodeq0g  15556  fprodmodd  15559  rpnnen2lem10  15784  rpnnen2lem11  15785  sumeven  15948  sumodd  15949  lcmfunsnlem2  16197  oddprmge3  16257  oddprm  16363  nnoddn2prm  16364  nnoddn2prmb  16366  iserodd  16388  prmreclem2  16470  prmreclem3  16471  prmreclem5  16473  4sqlem19  16516  prmdvdsprmo  16595  prmodvdslcmf  16600  prmlem0  16659  firest  16937  grpinvnzcl  18435  symgextfv  18810  pmtrf  18847  pmtrdifellem3  18870  sylow2alem2  19007  sylow2a  19008  efgsf  19119  efgsrel  19124  efgs1  19125  efgsfo  19129  gsumzaddlem  19306  gsumzadd  19307  gsumzmhm  19322  gsum2d2lem  19358  dprdfadd  19407  dprdres  19415  subgdmdprd  19421  dmdprdsplitlem  19424  dmdprdsplit2lem  19432  dpjidcl  19445  ablfac1b  19457  pgpfac1lem1  19461  gsummgp0  19626  isirred  19717  irredrmul  19725  isdrng2  19777  isdrngd  19792  cntzsdrg  19846  lcomfsupp  19939  lbspropd  20136  lspsneq  20159  lsppratlem6  20189  lbsextlem2  20196  lbsextlem4  20198  ringelnzr  20304  xrs1mnd  20401  xrs10  20402  xrs1cmn  20403  cnsubrg  20423  psgnodpm  20550  zrhpsgnodpm  20554  evpmodpmf1o  20558  uvcresum  20755  frlmssuvc1  20756  frlmsslsp  20758  frlmup2  20761  lindfrn  20783  f1lindf  20784  lindfmm  20789  islindf4  20800  psrbaglesupp  20883  psrbaglesuppOLD  20884  psrlidm  20928  psrridm  20929  mplsubglem  20961  mpllsslem  20962  mplsubrglem  20966  mplmonmul  20993  mplcoe1  20994  mplcoe5  20997  mplbas2  20999  evlslem3  21040  mhpvscacl  21094  coe1tmmul2  21197  coe1tmmul  21198  dmatmul  21394  1marepvsma1  21480  mdetdiaglem  21495  mdetrlin  21499  mdetrsca  21500  mdetralt  21505  maducoeval2  21537  madugsum  21540  symgmatr01  21551  gsummatr01lem3  21554  gsummatr01lem4  21555  gsummatr01  21556  smadiadetlem0  21558  smadiadetlem1a  21560  cmpfi  22305  2ndcdisj2  22354  elptr2  22471  ptcnplem  22518  xkopt  22552  kqdisj  22629  fin1aufil  22829  ptcmplem2  22950  ptcmplem3  22951  ptcmplem4  22952  opnsubg  23005  lpbl  23401  blcld  23403  zcld  23710  recld2  23711  reconnlem1  23723  divcn  23765  iundisj  24445  mbfeqalem1  24538  itg1val2  24581  itg1ge0  24583  i1fmullem  24591  i1fadd  24592  itg1addlem4  24596  itg1addlem4OLD  24597  itg1mulc  24602  itg1lea  24610  itg1le  24611  mbfi1fseqlem4  24616  itg2uba  24641  itg2lea  24642  itg2eqa  24643  itg2splitlem  24646  itg2split  24647  itgeqa  24711  ellimc3  24776  dvaddbr  24835  dvmulbr  24836  dvcobr  24843  dvcjbr  24846  dvrec  24852  dvrecg  24870  dvcnvlem  24873  dvexp3  24875  dveflem  24876  tdeglem4  24957  tdeglem4OLD  24958  deg1n0ima  24987  deg1mul3le  25014  ig1peu  25069  ply1termlem  25097  plypf1  25106  plyaddlem1  25107  plymullem1  25108  coeeulem  25118  coeidlem  25131  coeid3  25134  coefv0  25142  coemulhi  25148  coemulc  25149  dvply1  25177  fta1  25201  vieta1lem2  25204  elaa  25209  elqaalem2  25213  aannenlem2  25222  aaliou2  25233  tayl0  25254  dvtaylp  25262  taylthlem1  25265  taylthlem2  25266  pserdvlem2  25320  logbcl  25650  relogbreexp  25658  relogbcxp  25668  cxplogb  25669  dcubic  25729  rlimcnp  25848  jensen  25871  dmgmaddn0  25905  dmlogdmgm  25906  lgamgulmlem2  25912  igamz  25930  gamp1  25940  regamcl  25943  wilthlem2  25951  basellem3  25965  chpub  26101  logexprlim  26106  lgslem1  26178  lgslem4  26181  lgsvalmod  26197  lgsqr  26232  lgsqrmod  26233  lgsqrmodndvds  26234  gausslemma2dlem0b  26238  gausslemma2dlem0c  26239  gausslemma2dlem0i  26245  gausslemma2dlem1a  26246  gausslemma2dlem4  26250  gausslemma2dlem5a  26251  gausslemma2dlem7  26254  gausslemma2d  26255  lgsquad2  26267  m1lgs  26269  2lgsoddprm  26297  2sqreultblem  26329  dchrisum0fno1  26392  rplogsum  26408  ishpg  26850  elntg2  27076  umgrislfupgrlem  27213  usgruspgrb  27272  nbumgrvtx  27434  nbupgrres  27452  isuvtx  27483  cusgrexilem2  27530  cusgrexi  27531  structtocusgr  27534  cusgrres  27536  cusgrfilem2  27544  vtxdginducedm1  27631  cusconngr  28274  2pthfrgr  28367  frgrncvvdeq  28392  frgrwopreglem4  28398  frgrwopreglem5  28404  frgrwopreg  28406  frgrhash2wsp  28415  strlem1  30331  strlem3  30334  strlem4  30335  strlem5  30336  hstrlem3  30342  hstrlem4  30343  iundisjf  30647  suppss3  30779  iundisjfi  30837  qtophaus  31500  elzdif0  31642  ind0  31698  measvunilem  31892  sibfof  32019  eulerpartlemb  32047  eulerpartlemf  32049  sseqf  32071  ballotlem5  32178  ballotlemi1  32181  ballotlemii  32182  ballotlemic  32185  ballotlem1c  32186  ballotlemscr  32197  ballotlemro  32201  ballotlemfg  32204  ballotlemfrc  32205  ballotlemfrceq  32207  ballotlemrinv0  32211  plymulx0  32238  signstfvn  32260  signsvfn  32273  bnj923  32460  bnj570  32598  bnj594  32605  subfacp1lem1  32854  satffunlem2lem1  33079  mrsubcn  33194  mrsubco  33196  circum  33345  dfon2lem6  33483  ttrcltr  33515  xpord2pred  33529  neibastop1  34285  bj-restn0b  34997  lindsadd  35507  lindsenlbs  35509  matunitlindflem1  35510  poimirlem24  35538  poimirlem25  35539  dvtan  35564  itg2addnclem2  35566  ftc1cnnc  35586  dvasin  35598  dvreasin  35600  dvreacos  35601  isdrngo2  35853  isdrngo3  35854  divrngidl  35923  isfldidl  35963  pridlc2  35967  pridlc3  35968  prter2  36632  lsateln0  36746  lsatlss  36747  lsmsat  36759  lsatcv0  36782  lsat0cv  36784  lcv1  36792  l1cvpat  36805  dih1dimatlem  39080  dihatexv2  39090  djhcvat42  39166  dihjat1lem  39179  dochsatshp  39202  lcfl6  39251  mapdrvallem2  39396  mapdpglem32  39456  sticksstones22  39846  isdomn4  39894  evlsbagval  39985  prjspertr  40152  prjsperref  40153  prjspersym  40154  prjspvs  40157  prjsprellsp  40158  dffltz  40174  irrapx1  40353  pell1234qrne0  40378  pell1234qrreccl  40379  pell1234qrmulcl  40380  pell14qrgt0  40384  pell1234qrdich  40386  pell14qrdich  40394  pell1qrge1  40395  pell1qr1  40396  pell1qrgap  40399  pell14qrgapw  40401  pellqrexplicit  40402  pellqrex  40404  pellfundge  40407  pellfundgt1  40408  setindtr  40549  kelac1  40591  mpaaeu  40678  flcidc  40702  deg1mhm  40735  radcnvrat  41605  binomcxplemdvbinom  41644  disjiun2  42279  fiiuncl  42286  disjf1o  42402  difmapsn  42425  supminfxr2  42684  icoiccdif  42737  iccdificc  42752  fsumnncl  42788  fsumsupp0  42794  fprod0  42812  climrec  42819  islpcn  42855  lptre2pt  42856  limclner  42867  cnrefiisplem  43045  fprodcncf  43116  fperdvper  43135  dvdivcncf  43143  dvnmul  43159  dvmptfprodlem  43160  dvnprodlem2  43163  stoweidlem25  43241  stoweidlem28  43244  stoweidlem41  43257  stoweidlem44  43260  stoweidlem46  43262  stirlinglem5  43294  dirkercncflem1  43319  dirkercncflem2  43320  fourierdlem24  43347  fourierdlem62  43384  fouriersw  43447  fouriercn  43448  elaa2lem  43449  elaa2  43450  etransclem25  43475  etransclem35  43485  etransclem44  43494  sge0iunmptlemfi  43626  sge0fodjrnlem  43629  iundjiunlem  43672  meadjiunlem  43678  meaiininclem  43699  isomenndlem  43743  hsphoidmvle2  43798  hsphoidmvle  43799  hoidmv1lelem2  43805  hoidmvle  43813  ovnhoilem1  43814  hspdifhsp  43829  hspmbllem2  43840  ovnsubadd2lem  43858  ovolval4lem1  43862  preimagelt  43911  preimalegt  43912  fsummsndifre  44497  fsummmodsndifre  44499  odz2prm2pw  44688  fmtnoprmfac1lem  44689  fmtnoprmfac2lem1  44691  2pwp1prm  44714  lighneallem2  44731  lighneallem3  44732  lighneallem4  44735  bgoldbtbndlem2  44931  bgoldbtbndlem3  44932  bgoldbtbndlem4  44933  bgoldbtbnd  44934  c0rhm  45143  c0rnghm  45144  zrrnghm  45148  2zrngnmlid2  45182  zrinitorngc  45231  zrtermorngc  45232  mgpsumunsn  45370  mgpsumz  45371  mgpsumn  45372  lindslinindsimp1  45471  lindslinindsimp2  45477  lincresunit1  45491  lincresunit2  45492  lincresunit3lem1  45493  lincresunit3lem2  45494  lincresunit3  45495  lindssnlvec  45500  logcxp0  45554  relogbmulbexp  45580  relogbdivb  45581  dignn0fr  45620  rrxlinesc  45754  eenglngeehlnmlem1  45756  eenglngeehlnmlem2  45757