Theorem eldifi 4126

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2107   ∖ cdif 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3951

This theorem is referenced by:  difss  4131  eqoreldif  4688  xpdifid  6165  tz7.7  6388  tfi  7839  peano5  7881  peano5OLD  7882  xpord2pred  8128  frrlem12  8279  frrlem13  8280  wfrlem10OLD  8315  wfrlem15OLD  8320  tz7.48-1  8440  tz7.49  8442  dif20el  8502  oaf1o  8560  oeordi  8584  oeord  8585  oecan  8586  oeword  8587  oeworde  8590  oelimcl  8597  oeeulem  8598  oeeui  8599  oaabs2  8645  boxcutc  8932  domdifsn  9051  pssnn  9165  pwfilem  9174  isinf  9257  isinfOLD  9258  pssnnOLD  9262  pwfilemOLD  9343  fsuppco2  9395  fsuppcor  9396  ordtypelem7  9516  unxpwdom2  9580  inf3lem3  9622  cantnfp1lem1  9670  cantnfp1lem3  9672  ttrcltr  9708  infxpenc2lem1  10011  dfacacn  10133  isf32lem3  10347  isf34lem4  10369  fin67  10387  isfin7-2  10388  domtriomlem  10434  axdc2lem  10440  axdc3lem4  10445  axdc4lem  10447  ttukeylem7  10507  konigthlem  10560  fpwwe2lem12  10634  fpwwe2  10635  modfzo0difsn  13905  hashf1lem1  14412  hashf1lem1OLD  14413  hashle2prv  14436  rlimrege0  15520  rlimrecl  15521  sumrblem  15654  fsumcvg  15655  summolem2a  15658  fsumss  15668  fsumsplit1  15688  fsumless  15739  cvgcmpce  15761  binomlem  15772  incexclem  15779  incexc  15780  isumltss  15791  prodrblem  15870  fprodcvg  15871  prodmolem2a  15875  fprodss  15889  fprodn0f  15932  fprodeq0g  15935  fprodmodd  15938  rpnnen2lem10  16163  rpnnen2lem11  16164  sumeven  16327  sumodd  16328  lcmfunsnlem2  16574  oddprmge3  16634  oddprm  16740  nnoddn2prm  16741  nnoddn2prmb  16743  iserodd  16765  prmreclem2  16847  prmreclem3  16848  prmreclem5  16850  4sqlem19  16893  prmdvdsprmo  16972  prmodvdslcmf  16977  prmlem0  17036  firest  17375  grpinvnzcl  18892  symgextfv  19281  pmtrf  19318  pmtrdifellem3  19341  sylow2alem2  19481  sylow2a  19482  efgsf  19592  efgsrel  19597  efgs1  19598  efgsfo  19602  gsumzaddlem  19784  gsumzadd  19785  gsumzmhm  19800  gsum2d2lem  19836  dprdfadd  19885  dprdres  19893  subgdmdprd  19899  dmdprdsplitlem  19902  dmdprdsplit2lem  19910  dpjidcl  19923  ablfac1b  19935  pgpfac1lem1  19939  gsummgp0  20124  isirred  20226  irredrmul  20234  ringelnzr  20293  isdrng2  20322  isdrngd  20341  isdrngdOLD  20343  imadrhmcl  20406  cntzsdrg  20411  lcomfsupp  20505  lbspropd  20703  lspsneq  20728  lsppratlem6  20758  lbsextlem2  20765  lbsextlem4  20767  isdomn4  20911  xrs1mnd  20976  xrs10  20977  xrs1cmn  20978  cnsubrg  20998  psgnodpm  21133  zrhpsgnodpm  21137  evpmodpmf1o  21141  uvcresum  21340  frlmssuvc1  21341  frlmsslsp  21343  frlmup2  21346  lindfrn  21368  f1lindf  21369  lindfmm  21374  islindf4  21385  psrbaglesupp  21469  psrbaglesuppOLD  21470  psrlidm  21515  psrridm  21516  mplsubglem  21550  mpllsslem  21551  mplsubrglem  21555  mplmonmul  21583  mplcoe1  21584  mplcoe5  21587  mplbas2  21589  evlslem3  21635  mhpvscacl  21689  coe1tmmul2  21790  coe1tmmul  21791  dmatmul  21991  1marepvsma1  22077  mdetdiaglem  22092  mdetrlin  22096  mdetrsca  22097  mdetralt  22102  maducoeval2  22134  madugsum  22137  symgmatr01  22148  gsummatr01lem3  22151  gsummatr01lem4  22152  gsummatr01  22153  smadiadetlem0  22155  smadiadetlem1a  22157  cmpfi  22904  2ndcdisj2  22953  elptr2  23070  ptcnplem  23117  xkopt  23151  kqdisj  23228  fin1aufil  23428  ptcmplem2  23549  ptcmplem3  23550  ptcmplem4  23551  opnsubg  23604  lpbl  24004  blcld  24006  zcld  24321  recld2  24322  reconnlem1  24334  divcn  24376  iundisj  25057  mbfeqalem1  25150  itg1val2  25193  itg1ge0  25195  i1fmullem  25203  i1fadd  25204  itg1addlem4  25208  itg1addlem4OLD  25209  itg1mulc  25214  itg1lea  25222  itg1le  25223  mbfi1fseqlem4  25228  itg2uba  25253  itg2lea  25254  itg2eqa  25255  itg2splitlem  25258  itg2split  25259  itgeqa  25323  ellimc3  25388  dvaddbr  25447  dvmulbr  25448  dvcobr  25455  dvcjbr  25458  dvrec  25464  dvrecg  25482  dvcnvlem  25485  dvexp3  25487  dveflem  25488  tdeglem4  25569  tdeglem4OLD  25570  deg1n0ima  25599  deg1mul3le  25626  ig1peu  25681  ply1termlem  25709  plypf1  25718  plyaddlem1  25719  plymullem1  25720  coeeulem  25730  coeidlem  25743  coeid3  25746  coefv0  25754  coemulhi  25760  coemulc  25761  dvply1  25789  fta1  25813  vieta1lem2  25816  elaa  25821  elqaalem2  25825  aannenlem2  25834  aaliou2  25845  tayl0  25866  dvtaylp  25874  taylthlem1  25877  taylthlem2  25878  pserdvlem2  25932  logbcl  26262  relogbreexp  26270  relogbcxp  26280  cxplogb  26281  dcubic  26341  rlimcnp  26460  jensen  26483  dmgmaddn0  26517  dmlogdmgm  26518  lgamgulmlem2  26524  igamz  26542  gamp1  26552  regamcl  26555  wilthlem2  26563  basellem3  26577  chpub  26713  logexprlim  26718  lgslem1  26790  lgslem4  26793  lgsvalmod  26809  lgsqr  26844  lgsqrmod  26845  lgsqrmodndvds  26846  gausslemma2dlem0b  26850  gausslemma2dlem0c  26851  gausslemma2dlem0i  26857  gausslemma2dlem1a  26858  gausslemma2dlem4  26862  gausslemma2dlem5a  26863  gausslemma2dlem7  26866  gausslemma2d  26867  lgsquad2  26879  m1lgs  26881  2lgsoddprm  26909  2sqreultblem  26941  dchrisum0fno1  27004  rplogsum  27020  ishpg  28000  elntg2  28233  umgrislfupgrlem  28372  usgruspgrb  28431  nbumgrvtx  28593  nbupgrres  28611  isuvtx  28642  cusgrexilem2  28689  cusgrexi  28690  structtocusgr  28693  cusgrres  28695  cusgrfilem2  28703  vtxdginducedm1  28790  cusconngr  29434  2pthfrgr  29527  frgrncvvdeq  29552  frgrwopreglem4  29558  frgrwopreglem5  29564  frgrwopreg  29566  frgrhash2wsp  29575  strlem1  31491  strlem3  31494  strlem4  31495  strlem5  31496  hstrlem3  31502  hstrlem4  31503  iundisjf  31808  suppss3  31937  iundisjfi  31995  suppssnn0  32005  qsdrngi  32598  irngnzply1  32744  qtophaus  32805  elzdif0  32949  ind0  33005  measvunilem  33199  sibfof  33328  eulerpartlemb  33356  eulerpartlemf  33358  sseqf  33380  ballotlem5  33487  ballotlemi1  33490  ballotlemii  33491  ballotlemic  33494  ballotlem1c  33495  ballotlemscr  33506  ballotlemro  33510  ballotlemfg  33513  ballotlemfrc  33514  ballotlemfrceq  33516  ballotlemrinv0  33520  plymulx0  33547  signstfvn  33569  signsvfn  33582  bnj923  33768  bnj570  33905  bnj594  33912  subfacp1lem1  34159  satffunlem2lem1  34384  mrsubcn  34499  mrsubco  34501  circum  34648  dfon2lem6  34749  gg-divcn  35152  gg-dvmulbr  35164  gg-dvcobr  35165  neibastop1  35233  bj-restn0b  35961  lindsadd  36470  lindsenlbs  36472  matunitlindflem1  36473  poimirlem24  36501  poimirlem25  36502  dvtan  36527  itg2addnclem2  36529  ftc1cnnc  36549  dvasin  36561  dvreasin  36563  dvreacos  36564  isdrngo2  36815  isdrngo3  36816  divrngidl  36885  isfldidl  36925  pridlc2  36929  pridlc3  36930  prter2  37740  lsateln0  37854  lsatlss  37855  lsmsat  37867  lsatcv0  37890  lsat0cv  37892  lcv1  37900  l1cvpat  37913  dih1dimatlem  40189  dihatexv2  40199  djhcvat42  40275  dihjat1lem  40288  dochsatshp  40311  lcfl6  40360  mapdrvallem2  40505  mapdpglem32  40565  sticksstones22  40973  evlsvvvallem  41131  evlsvvvallem2  41132  evlsvvval  41133  evlsbagval  41136  selvvvval  41155  evlselv  41157  evlsmhpvvval  41165  prjspertr  41344  prjsperref  41345  prjspersym  41346  prjspvs  41349  prjsprellsp  41350  dffltz  41373  irrapx1  41552  pell1234qrne0  41577  pell1234qrreccl  41578  pell1234qrmulcl  41579  pell14qrgt0  41583  pell1234qrdich  41585  pell14qrdich  41593  pell1qrge1  41594  pell1qr1  41595  pell1qrgap  41598  pell14qrgapw  41600  pellqrexplicit  41601  pellqrex  41603  pellfundge  41606  pellfundgt1  41607  setindtr  41749  kelac1  41791  mpaaeu  41878  flcidc  41902  deg1mhm  41935  onexoegt  41979  cantnfub  42057  cantnfresb  42060  succlg  42064  dflim5  42065  onmcl  42067  omabs2  42068  tfsconcatrev  42084  minregex2  42272  radcnvrat  43059  binomcxplemdvbinom  43098  disjiun2  43731  fiiuncl  43738  disjf1o  43875  difmapsn  43897  supminfxr2  44166  icoiccdif  44224  iccdificc  44239  fsumnncl  44275  fsumsupp0  44281  fprod0  44299  climrec  44306  islpcn  44342  lptre2pt  44343  limclner  44354  cnrefiisplem  44532  fprodcncf  44603  fperdvper  44622  dvdivcncf  44630  dvnmul  44646  dvmptfprodlem  44647  dvnprodlem2  44650  stoweidlem25  44728  stoweidlem28  44731  stoweidlem41  44744  stoweidlem44  44747  stoweidlem46  44749  stirlinglem5  44781  dirkercncflem1  44806  dirkercncflem2  44807  fourierdlem24  44834  fourierdlem62  44871  fouriersw  44934  fouriercn  44935  elaa2lem  44936  elaa2  44937  etransclem25  44962  etransclem35  44972  etransclem44  44981  sge0iunmptlemfi  45116  sge0fodjrnlem  45119  iundjiunlem  45162  meadjiunlem  45168  meaiininclem  45189  isomenndlem  45233  hsphoidmvle2  45288  hsphoidmvle  45289  hoidmv1lelem2  45295  hoidmvle  45303  ovnhoilem1  45304  hspdifhsp  45319  hspmbllem2  45330  ovnsubadd2lem  45348  ovolval4lem1  45352  preimagelt  45402  preimalegt  45403  fsummsndifre  46027  fsummmodsndifre  46029  odz2prm2pw  46218  fmtnoprmfac1lem  46219  fmtnoprmfac2lem1  46221  2pwp1prm  46244  lighneallem2  46261  lighneallem3  46262  lighneallem4  46265  bgoldbtbndlem2  46461  bgoldbtbndlem3  46462  bgoldbtbndlem4  46463  bgoldbtbnd  46464  c0rhm  46697  c0rnghm  46698  zrrnghm  46702  2zrngnmlid2  46803  zrinitorngc  46852  zrtermorngc  46853  mgpsumunsn  46991  mgpsumz  46992  mgpsumn  46993  lindslinindsimp1  47092  lindslinindsimp2  47098  lincresunit1  47112  lincresunit2  47113  lincresunit3lem1  47114  lincresunit3lem2  47115  lincresunit3  47116  lindssnlvec  47121  logcxp0  47175  relogbmulbexp  47201  relogbdivb  47202  dignn0fr  47241  rrxlinesc  47375  eenglngeehlnmlem1  47377  eenglngeehlnmlem2  47378