Theorem eldifi 4066

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-dif 3895

This theorem is referenced by:  difss  4071  eqoreldif  4626  xpdifid  6070  tz7.7  6291  tfi  7694  peano5  7734  peano5OLD  7735  frrlem12  8104  frrlem13  8105  wfrlem10OLD  8140  wfrlem15OLD  8145  tz7.48-1  8265  tz7.49  8267  dif20el  8320  oaf1o  8379  oeordi  8403  oeord  8404  oecan  8405  oeword  8406  oeworde  8409  oelimcl  8416  oeeulem  8417  oeeui  8418  oaabs2  8462  boxcutc  8712  domdifsn  8824  pssnn  8933  pwfilem  8942  isinf  9014  pssnnOLD  9018  pwfilemOLD  9091  fsuppco2  9140  fsuppcor  9141  ordtypelem7  9261  unxpwdom2  9325  inf3lem3  9366  cantnfp1lem1  9414  cantnfp1lem3  9416  ttrcltr  9452  infxpenc2lem1  9776  dfacacn  9898  isf32lem3  10112  isf34lem4  10134  fin67  10152  isfin7-2  10153  domtriomlem  10199  axdc2lem  10205  axdc3lem4  10210  axdc4lem  10212  ttukeylem7  10272  konigthlem  10325  fpwwe2lem12  10399  fpwwe2  10400  modfzo0difsn  13661  hashf1lem1  14166  hashf1lem1OLD  14167  hashle2prv  14190  rlimrege0  15286  rlimrecl  15287  sumrblem  15421  fsumcvg  15422  summolem2a  15425  fsumss  15435  fsumsplit1  15455  fsumless  15506  cvgcmpce  15528  binomlem  15539  incexclem  15546  incexc  15547  isumltss  15558  prodrblem  15637  fprodcvg  15638  prodmolem2a  15642  fprodss  15656  fprodn0f  15699  fprodeq0g  15702  fprodmodd  15705  rpnnen2lem10  15930  rpnnen2lem11  15931  sumeven  16094  sumodd  16095  lcmfunsnlem2  16343  oddprmge3  16403  oddprm  16509  nnoddn2prm  16510  nnoddn2prmb  16512  iserodd  16534  prmreclem2  16616  prmreclem3  16617  prmreclem5  16619  4sqlem19  16662  prmdvdsprmo  16741  prmodvdslcmf  16746  prmlem0  16805  firest  17141  grpinvnzcl  18645  symgextfv  19024  pmtrf  19061  pmtrdifellem3  19084  sylow2alem2  19221  sylow2a  19222  efgsf  19333  efgsrel  19338  efgs1  19339  efgsfo  19343  gsumzaddlem  19520  gsumzadd  19521  gsumzmhm  19536  gsum2d2lem  19572  dprdfadd  19621  dprdres  19629  subgdmdprd  19635  dmdprdsplitlem  19638  dmdprdsplit2lem  19646  dpjidcl  19659  ablfac1b  19671  pgpfac1lem1  19675  gsummgp0  19845  isirred  19939  irredrmul  19947  isdrng2  19999  isdrngd  20014  cntzsdrg  20068  lcomfsupp  20161  lbspropd  20359  lspsneq  20382  lsppratlem6  20412  lbsextlem2  20419  lbsextlem4  20421  ringelnzr  20535  xrs1mnd  20634  xrs10  20635  xrs1cmn  20636  cnsubrg  20656  psgnodpm  20791  zrhpsgnodpm  20795  evpmodpmf1o  20799  uvcresum  20998  frlmssuvc1  20999  frlmsslsp  21001  frlmup2  21004  lindfrn  21026  f1lindf  21027  lindfmm  21032  islindf4  21043  psrbaglesupp  21125  psrbaglesuppOLD  21126  psrlidm  21170  psrridm  21171  mplsubglem  21203  mpllsslem  21204  mplsubrglem  21208  mplmonmul  21235  mplcoe1  21236  mplcoe5  21239  mplbas2  21241  evlslem3  21288  mhpvscacl  21342  coe1tmmul2  21445  coe1tmmul  21446  dmatmul  21644  1marepvsma1  21730  mdetdiaglem  21745  mdetrlin  21749  mdetrsca  21750  mdetralt  21755  maducoeval2  21787  madugsum  21790  symgmatr01  21801  gsummatr01lem3  21804  gsummatr01lem4  21805  gsummatr01  21806  smadiadetlem0  21808  smadiadetlem1a  21810  cmpfi  22557  2ndcdisj2  22606  elptr2  22723  ptcnplem  22770  xkopt  22804  kqdisj  22881  fin1aufil  23081  ptcmplem2  23202  ptcmplem3  23203  ptcmplem4  23204  opnsubg  23257  lpbl  23657  blcld  23659  zcld  23974  recld2  23975  reconnlem1  23987  divcn  24029  iundisj  24710  mbfeqalem1  24803  itg1val2  24846  itg1ge0  24848  i1fmullem  24856  i1fadd  24857  itg1addlem4  24861  itg1addlem4OLD  24862  itg1mulc  24867  itg1lea  24875  itg1le  24876  mbfi1fseqlem4  24881  itg2uba  24906  itg2lea  24907  itg2eqa  24908  itg2splitlem  24911  itg2split  24912  itgeqa  24976  ellimc3  25041  dvaddbr  25100  dvmulbr  25101  dvcobr  25108  dvcjbr  25111  dvrec  25117  dvrecg  25135  dvcnvlem  25138  dvexp3  25140  dveflem  25141  tdeglem4  25222  tdeglem4OLD  25223  deg1n0ima  25252  deg1mul3le  25279  ig1peu  25334  ply1termlem  25362  plypf1  25371  plyaddlem1  25372  plymullem1  25373  coeeulem  25383  coeidlem  25396  coeid3  25399  coefv0  25407  coemulhi  25413  coemulc  25414  dvply1  25442  fta1  25466  vieta1lem2  25469  elaa  25474  elqaalem2  25478  aannenlem2  25487  aaliou2  25498  tayl0  25519  dvtaylp  25527  taylthlem1  25530  taylthlem2  25531  pserdvlem2  25585  logbcl  25915  relogbreexp  25923  relogbcxp  25933  cxplogb  25934  dcubic  25994  rlimcnp  26113  jensen  26136  dmgmaddn0  26170  dmlogdmgm  26171  lgamgulmlem2  26177  igamz  26195  gamp1  26205  regamcl  26208  wilthlem2  26216  basellem3  26230  chpub  26366  logexprlim  26371  lgslem1  26443  lgslem4  26446  lgsvalmod  26462  lgsqr  26497  lgsqrmod  26498  lgsqrmodndvds  26499  gausslemma2dlem0b  26503  gausslemma2dlem0c  26504  gausslemma2dlem0i  26510  gausslemma2dlem1a  26511  gausslemma2dlem4  26515  gausslemma2dlem5a  26516  gausslemma2dlem7  26519  gausslemma2d  26520  lgsquad2  26532  m1lgs  26534  2lgsoddprm  26562  2sqreultblem  26594  dchrisum0fno1  26657  rplogsum  26673  ishpg  27118  elntg2  27351  umgrislfupgrlem  27490  usgruspgrb  27549  nbumgrvtx  27711  nbupgrres  27729  isuvtx  27760  cusgrexilem2  27807  cusgrexi  27808  structtocusgr  27811  cusgrres  27813  cusgrfilem2  27821  vtxdginducedm1  27908  cusconngr  28551  2pthfrgr  28644  frgrncvvdeq  28669  frgrwopreglem4  28675  frgrwopreglem5  28681  frgrwopreg  28683  frgrhash2wsp  28692  strlem1  30608  strlem3  30611  strlem4  30612  strlem5  30613  hstrlem3  30619  hstrlem4  30620  iundisjf  30924  suppss3  31055  iundisjfi  31113  qtophaus  31782  elzdif0  31926  ind0  31982  measvunilem  32176  sibfof  32303  eulerpartlemb  32331  eulerpartlemf  32333  sseqf  32355  ballotlem5  32462  ballotlemi1  32465  ballotlemii  32466  ballotlemic  32469  ballotlem1c  32470  ballotlemscr  32481  ballotlemro  32485  ballotlemfg  32488  ballotlemfrc  32489  ballotlemfrceq  32491  ballotlemrinv0  32495  plymulx0  32522  signstfvn  32544  signsvfn  32557  bnj923  32744  bnj570  32881  bnj594  32888  subfacp1lem1  33137  satffunlem2lem1  33362  mrsubcn  33477  mrsubco  33479  circum  33628  dfon2lem6  33760  xpord2pred  33788  neibastop1  34544  bj-restn0b  35258  lindsadd  35766  lindsenlbs  35768  matunitlindflem1  35769  poimirlem24  35797  poimirlem25  35798  dvtan  35823  itg2addnclem2  35825  ftc1cnnc  35845  dvasin  35857  dvreasin  35859  dvreacos  35860  isdrngo2  36112  isdrngo3  36113  divrngidl  36182  isfldidl  36222  pridlc2  36226  pridlc3  36227  prter2  36891  lsateln0  37005  lsatlss  37006  lsmsat  37018  lsatcv0  37041  lsat0cv  37043  lcv1  37051  l1cvpat  37064  dih1dimatlem  39339  dihatexv2  39349  djhcvat42  39425  dihjat1lem  39438  dochsatshp  39461  lcfl6  39510  mapdrvallem2  39655  mapdpglem32  39715  sticksstones22  40121  isdomn4  40169  evlsbagval  40272  prjspertr  40441  prjsperref  40442  prjspersym  40443  prjspvs  40446  prjsprellsp  40447  prjcrv0  40467  dffltz  40468  irrapx1  40647  pell1234qrne0  40672  pell1234qrreccl  40673  pell1234qrmulcl  40674  pell14qrgt0  40678  pell1234qrdich  40680  pell14qrdich  40688  pell1qrge1  40689  pell1qr1  40690  pell1qrgap  40693  pell14qrgapw  40695  pellqrexplicit  40696  pellqrex  40698  pellfundge  40701  pellfundgt1  40702  setindtr  40843  kelac1  40885  mpaaeu  40972  flcidc  40996  deg1mhm  41029  radcnvrat  41902  binomcxplemdvbinom  41941  disjiun2  42576  fiiuncl  42583  disjf1o  42699  difmapsn  42722  supminfxr2  42980  icoiccdif  43033  iccdificc  43048  fsumnncl  43084  fsumsupp0  43090  fprod0  43108  climrec  43115  islpcn  43151  lptre2pt  43152  limclner  43163  cnrefiisplem  43341  fprodcncf  43412  fperdvper  43431  dvdivcncf  43439  dvnmul  43455  dvmptfprodlem  43456  dvnprodlem2  43459  stoweidlem25  43537  stoweidlem28  43540  stoweidlem41  43553  stoweidlem44  43556  stoweidlem46  43558  stirlinglem5  43590  dirkercncflem1  43615  dirkercncflem2  43616  fourierdlem24  43643  fourierdlem62  43680  fouriersw  43743  fouriercn  43744  elaa2lem  43745  elaa2  43746  etransclem25  43771  etransclem35  43781  etransclem44  43790  sge0iunmptlemfi  43922  sge0fodjrnlem  43925  iundjiunlem  43968  meadjiunlem  43974  meaiininclem  43995  isomenndlem  44039  hsphoidmvle2  44094  hsphoidmvle  44095  hoidmv1lelem2  44101  hoidmvle  44109  ovnhoilem1  44110  hspdifhsp  44125  hspmbllem2  44136  ovnsubadd2lem  44154  ovolval4lem1  44158  preimagelt  44207  preimalegt  44208  fsummsndifre  44793  fsummmodsndifre  44795  odz2prm2pw  44984  fmtnoprmfac1lem  44985  fmtnoprmfac2lem1  44987  2pwp1prm  45010  lighneallem2  45027  lighneallem3  45028  lighneallem4  45031  bgoldbtbndlem2  45227  bgoldbtbndlem3  45228  bgoldbtbndlem4  45229  bgoldbtbnd  45230  c0rhm  45439  c0rnghm  45440  zrrnghm  45444  2zrngnmlid2  45478  zrinitorngc  45527  zrtermorngc  45528  mgpsumunsn  45666  mgpsumz  45667  mgpsumn  45668  lindslinindsimp1  45767  lindslinindsimp2  45773  lincresunit1  45787  lincresunit2  45788  lincresunit3lem1  45789  lincresunit3lem2  45790  lincresunit3  45791  lindssnlvec  45796  logcxp0  45850  relogbmulbexp  45876  relogbdivb  45877  dignn0fr  45916  rrxlinesc  46050  eenglngeehlnmlem1  46052  eenglngeehlnmlem2  46053