Theorem eldifi 4123

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2099   ∖ cdif 3942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-dif 3948

This theorem is referenced by:  difss  4128  eqoreldif  4685  xpdifid  6167  tz7.7  6390  tfi  7852  peano5  7894  peano5OLD  7895  xpord2pred  8145  frrlem12  8297  frrlem13  8298  wfrlem10OLD  8333  wfrlem15OLD  8338  tz7.48-1  8458  tz7.49  8460  dif20el  8520  oaf1o  8578  oeordi  8602  oeord  8603  oecan  8604  oeword  8605  oeworde  8608  oelimcl  8615  oeeulem  8616  oeeui  8617  oaabs2  8664  boxcutc  8954  domdifsn  9073  pssnn  9187  pwfilem  9196  isinf  9279  isinfOLD  9280  pssnnOLD  9284  pwfilemOLD  9365  fsuppco2  9421  fsuppcor  9422  ordtypelem7  9542  unxpwdom2  9606  inf3lem3  9648  cantnfp1lem1  9696  cantnfp1lem3  9698  ttrcltr  9734  infxpenc2lem1  10037  dfacacn  10159  isf32lem3  10373  isf34lem4  10395  fin67  10413  isfin7-2  10414  domtriomlem  10460  axdc2lem  10466  axdc3lem4  10471  axdc4lem  10473  ttukeylem7  10533  konigthlem  10586  fpwwe2lem12  10660  fpwwe2  10661  modfzo0difsn  13935  hashf1lem1  14442  hashf1lem1OLD  14443  hashle2prv  14466  rlimrege0  15550  rlimrecl  15551  sumrblem  15684  fsumcvg  15685  summolem2a  15688  fsumss  15698  fsumsplit1  15718  fsumless  15769  cvgcmpce  15791  binomlem  15802  incexclem  15809  incexc  15810  isumltss  15821  prodrblem  15900  fprodcvg  15901  prodmolem2a  15905  fprodss  15919  fprodn0f  15962  fprodeq0g  15965  fprodmodd  15968  rpnnen2lem10  16194  rpnnen2lem11  16195  sumeven  16358  sumodd  16359  lcmfunsnlem2  16605  oddprmge3  16665  oddprm  16773  nnoddn2prm  16774  nnoddn2prmb  16776  iserodd  16798  prmreclem2  16880  prmreclem3  16881  prmreclem5  16883  4sqlem19  16926  prmdvdsprmo  17005  prmodvdslcmf  17010  prmlem0  17069  firest  17408  grpinvnzcl  18961  symgextfv  19367  pmtrf  19404  pmtrdifellem3  19427  sylow2alem2  19567  sylow2a  19568  efgsf  19678  efgsrel  19683  efgs1  19684  efgsfo  19688  gsumzaddlem  19870  gsumzadd  19871  gsumzmhm  19886  gsum2d2lem  19922  dprdfadd  19971  dprdres  19979  subgdmdprd  19985  dmdprdsplitlem  19988  dmdprdsplit2lem  19996  dpjidcl  20009  ablfac1b  20021  pgpfac1lem1  20025  gsummgp0  20248  isirred  20352  irredrmul  20360  ringelnzr  20454  c0rhm  20465  c0rnghm  20466  zrrnghm  20467  zrinitorngc  20569  zrtermorngc  20570  isdrng2  20632  isdrngd  20651  isdrngdOLD  20653  imadrhmcl  20679  cntzsdrg  20684  lcomfsupp  20779  lbspropd  20978  lspsneq  21004  lsppratlem6  21034  lbsextlem2  21041  lbsextlem4  21043  isdomn4  21244  xrs1mnd  21331  xrs10  21332  xrs1cmn  21333  cnsubrg  21354  psgnodpm  21514  zrhpsgnodpm  21518  evpmodpmf1o  21522  uvcresum  21721  frlmssuvc1  21722  frlmsslsp  21724  frlmup2  21727  lindfrn  21749  f1lindf  21750  lindfmm  21755  islindf4  21766  psrbaglesupp  21851  psrbaglesuppOLD  21852  psrlidm  21899  psrridm  21900  mplsubglem  21935  mpllsslem  21936  mplsubrglem  21940  mplmonmul  21968  mplcoe1  21969  mplcoe5  21972  mplbas2  21974  evlslem3  22020  mhpvscacl  22072  psdmul  22084  coe1tmmul2  22189  coe1tmmul  22190  dmatmul  22393  1marepvsma1  22479  mdetdiaglem  22494  mdetrlin  22498  mdetrsca  22499  mdetralt  22504  maducoeval2  22536  madugsum  22539  symgmatr01  22550  gsummatr01lem3  22553  gsummatr01lem4  22554  gsummatr01  22555  smadiadetlem0  22557  smadiadetlem1a  22559  cmpfi  23306  2ndcdisj2  23355  elptr2  23472  ptcnplem  23519  xkopt  23553  kqdisj  23630  fin1aufil  23830  ptcmplem2  23951  ptcmplem3  23952  ptcmplem4  23953  opnsubg  24006  lpbl  24406  blcld  24408  zcld  24723  recld2  24724  reconnlem1  24736  divcnOLD  24778  divcn  24780  iundisj  25471  mbfeqalem1  25564  itg1val2  25607  itg1ge0  25609  i1fmullem  25617  i1fadd  25618  itg1addlem4  25622  itg1addlem4OLD  25623  itg1mulc  25628  itg1lea  25636  itg1le  25637  mbfi1fseqlem4  25642  itg2uba  25667  itg2lea  25668  itg2eqa  25669  itg2splitlem  25672  itg2split  25673  itgeqa  25737  ellimc3  25802  dvaddbr  25862  dvmulbr  25863  dvmulbrOLD  25864  dvcobr  25871  dvcobrOLD  25872  dvcjbr  25875  dvrec  25881  dvrecg  25899  dvcnvlem  25902  dvexp3  25904  dveflem  25905  tdeglem4  25989  tdeglem4OLD  25990  deg1n0ima  26019  deg1mul3le  26046  ig1peu  26103  ply1termlem  26131  plypf1  26140  plyaddlem1  26141  plymullem1  26142  coeeulem  26152  coeidlem  26165  coeid3  26168  coefv0  26176  coemulhi  26182  coemulc  26183  dvply1  26212  fta1  26237  vieta1lem2  26240  elaa  26245  elqaalem2  26249  aannenlem2  26258  aaliou2  26269  tayl0  26290  dvtaylp  26299  taylthlem1  26302  taylthlem2  26303  taylthlem2OLD  26304  pserdvlem2  26359  logbcl  26693  relogbreexp  26701  relogbcxp  26711  cxplogb  26712  dcubic  26772  rlimcnp  26891  jensen  26915  dmgmaddn0  26949  dmlogdmgm  26950  lgamgulmlem2  26956  igamz  26974  gamp1  26984  regamcl  26987  wilthlem2  26995  basellem3  27009  chpub  27147  logexprlim  27152  lgslem1  27224  lgslem4  27227  lgsvalmod  27243  lgsqr  27278  lgsqrmod  27279  lgsqrmodndvds  27280  gausslemma2dlem0b  27284  gausslemma2dlem0c  27285  gausslemma2dlem0i  27291  gausslemma2dlem1a  27292  gausslemma2dlem4  27296  gausslemma2dlem5a  27297  gausslemma2dlem7  27300  gausslemma2d  27301  lgsquad2  27313  m1lgs  27315  2lgsoddprm  27343  2sqreultblem  27375  dchrisum0fno1  27438  rplogsum  27454  ishpg  28557  elntg2  28790  umgrislfupgrlem  28929  usgruspgrb  28990  nbumgrvtx  29153  nbupgrres  29171  isuvtx  29202  cusgrexilem2  29249  cusgrexi  29250  structtocusgr  29253  cusgrres  29256  cusgrfilem2  29264  vtxdginducedm1  29351  cusconngr  29995  2pthfrgr  30088  frgrncvvdeq  30113  frgrwopreglem4  30119  frgrwopreglem5  30125  frgrwopreg  30127  frgrhash2wsp  30136  strlem1  32054  strlem3  32057  strlem4  32058  strlem5  32059  hstrlem3  32065  hstrlem4  32066  iundisjf  32373  suppss3  32501  iundisjfi  32559  suppssnn0  32569  zringidom  32955  zringfrac  32991  qsdrngi  33201  irngnzply1  33360  qtophaus  33432  elzdif0  33576  ind0  33632  measvunilem  33826  sibfof  33955  eulerpartlemb  33983  eulerpartlemf  33985  sseqf  34007  ballotlem5  34114  ballotlemi1  34117  ballotlemii  34118  ballotlemic  34121  ballotlem1c  34122  ballotlemscr  34133  ballotlemro  34137  ballotlemfg  34140  ballotlemfrc  34141  ballotlemfrceq  34143  ballotlemrinv0  34147  plymulx0  34174  signstfvn  34196  signsvfn  34209  bnj923  34394  bnj570  34531  bnj594  34538  subfacp1lem1  34784  satffunlem2lem1  35009  mrsubcn  35124  mrsubco  35126  circum  35273  dfon2lem6  35379  neibastop1  35838  bj-restn0b  36565  lindsadd  37081  lindsenlbs  37083  matunitlindflem1  37084  poimirlem24  37112  poimirlem25  37113  dvtan  37138  itg2addnclem2  37140  ftc1cnnc  37160  dvasin  37172  dvreasin  37174  dvreacos  37175  isdrngo2  37426  isdrngo3  37427  divrngidl  37496  isfldidl  37536  pridlc2  37540  pridlc3  37541  prter2  38348  lsateln0  38462  lsatlss  38463  lsmsat  38475  lsatcv0  38498  lsat0cv  38500  lcv1  38508  l1cvpat  38521  dih1dimatlem  40797  dihatexv2  40807  djhcvat42  40883  dihjat1lem  40896  dochsatshp  40919  lcfl6  40968  mapdrvallem2  41113  mapdpglem32  41173  idomnnzgmulnz  41599  aks6d1c5lem3  41603  aks6d1c5lem2  41604  deg1gprod  41607  sticksstones22  41635  evlsvvvallem  41785  evlsvvvallem2  41786  evlsvvval  41787  evlsbagval  41790  selvvvval  41809  evlselv  41811  evlsmhpvvval  41819  prjspertr  42020  prjsperref  42021  prjspersym  42022  prjspvs  42025  prjsprellsp  42026  dffltz  42049  irrapx1  42239  pell1234qrne0  42264  pell1234qrreccl  42265  pell1234qrmulcl  42266  pell14qrgt0  42270  pell1234qrdich  42272  pell14qrdich  42280  pell1qrge1  42281  pell1qr1  42282  pell1qrgap  42285  pell14qrgapw  42287  pellqrexplicit  42288  pellqrex  42290  pellfundge  42293  pellfundgt1  42294  setindtr  42436  kelac1  42478  mpaaeu  42565  flcidc  42589  deg1mhm  42619  onexoegt  42663  cantnfub  42741  cantnfresb  42744  succlg  42748  dflim5  42749  onmcl  42751  omabs2  42752  tfsconcatrev  42768  minregex2  42956  radcnvrat  43742  binomcxplemdvbinom  43781  disjiun2  44413  fiiuncl  44420  disjf1o  44555  difmapsn  44576  supminfxr2  44842  icoiccdif  44900  iccdificc  44915  fsumnncl  44951  fsumsupp0  44957  fprod0  44975  climrec  44982  islpcn  45018  lptre2pt  45019  limclner  45030  cnrefiisplem  45208  fprodcncf  45279  fperdvper  45298  dvdivcncf  45306  dvnmul  45322  dvmptfprodlem  45323  dvnprodlem2  45326  stoweidlem25  45404  stoweidlem28  45407  stoweidlem41  45420  stoweidlem44  45423  stoweidlem46  45425  stirlinglem5  45457  dirkercncflem1  45482  dirkercncflem2  45483  fourierdlem24  45510  fourierdlem62  45547  fouriersw  45610  fouriercn  45611  elaa2lem  45612  elaa2  45613  etransclem25  45638  etransclem35  45648  etransclem44  45657  sge0iunmptlemfi  45792  sge0fodjrnlem  45795  iundjiunlem  45838  meadjiunlem  45844  meaiininclem  45865  isomenndlem  45909  hsphoidmvle2  45964  hsphoidmvle  45965  hoidmv1lelem2  45971  hoidmvle  45979  ovnhoilem1  45980  hspdifhsp  45995  hspmbllem2  46006  ovnsubadd2lem  46024  ovolval4lem1  46028  preimagelt  46078  preimalegt  46079  fsummsndifre  46703  fsummmodsndifre  46705  odz2prm2pw  46894  fmtnoprmfac1lem  46895  fmtnoprmfac2lem1  46897  2pwp1prm  46920  lighneallem2  46937  lighneallem3  46938  lighneallem4  46941  bgoldbtbndlem2  47137  bgoldbtbndlem3  47138  bgoldbtbndlem4  47139  bgoldbtbnd  47140  2zrngnmlid2  47310  mgpsumunsn  47416  mgpsumz  47417  mgpsumn  47418  lindslinindsimp1  47516  lindslinindsimp2  47522  lincresunit1  47536  lincresunit2  47537  lincresunit3lem1  47538  lincresunit3lem2  47539  lincresunit3  47540  lindssnlvec  47545  logcxp0  47599  relogbmulbexp  47625  relogbdivb  47626  dignn0fr  47665  rrxlinesc  47799  eenglngeehlnmlem1  47801  eenglngeehlnmlem2  47802