Theorem eldifi 4063

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   ∖ cdif 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3429  df-dif 3888

This theorem is referenced by:  difss  4068  eqoreldif  4619  xpdifid  6121  tz7.7  6338  tfi  7793  peano5  7833  resf1extb  7874  resf1ext2b  7875  xpord2pred  8084  frrlem12  8236  frrlem13  8237  tz7.48-1  8371  tz7.49  8373  dif20el  8429  oaf1o  8487  oeordi  8512  oeord  8513  oecan  8514  oeword  8515  oeworde  8518  oelimcl  8525  oeeulem  8526  oeeui  8527  oaabs2  8574  boxcutc  8878  domdifsn  8987  pssnn  9092  isinf  9164  pwfilem  9217  fsuppco2  9305  fsuppcor  9306  ordtypelem7  9428  unxpwdom2  9492  inf3lem3  9540  cantnfp1lem1  9588  cantnfp1lem3  9590  ttrcltr  9626  infxpenc2lem1  9930  dfacacn  10053  isf32lem3  10266  isf34lem4  10288  fin67  10306  isfin7-2  10307  domtriomlem  10353  axdc2lem  10359  axdc3lem4  10364  axdc4lem  10366  ttukeylem7  10426  konigthlem  10480  fpwwe2lem12  10554  fpwwe2  10555  ind0  12158  modfzo0difsn  13894  hashf1lem1  14406  hashle2prv  14429  rlimrege0  15530  rlimrecl  15531  sumrblem  15662  fsumcvg  15663  summolem2a  15666  fsumss  15676  fsumsplit1  15696  fsumless  15748  cvgcmpce  15770  binomlem  15783  incexclem  15790  incexc  15791  isumltss  15802  prodrblem  15883  fprodcvg  15884  prodmolem2a  15888  fprodss  15902  fprodn0f  15945  fprodeq0g  15948  fprodmodd  15951  rpnnen2lem10  16179  rpnnen2lem11  16180  sumeven  16345  sumodd  16346  lcmfunsnlem2  16598  oddprmge3  16659  oddprm  16770  nnoddn2prm  16771  nnoddn2prmb  16773  iserodd  16795  prmreclem2  16877  prmreclem3  16878  prmreclem5  16880  4sqlem19  16923  prmdvdsprmo  17002  prmodvdslcmf  17007  prmlem0  17065  firest  17384  chnccat  18581  chnrev  18582  grpinvnzcl  18976  symgextfv  19382  pmtrf  19419  pmtrdifellem3  19442  sylow2alem2  19582  sylow2a  19583  efgsf  19693  efgsrel  19698  efgs1  19699  efgsfo  19703  gsumzaddlem  19885  gsumzadd  19886  gsumzmhm  19901  gsum2d2lem  19937  dprdfadd  19986  dprdres  19994  subgdmdprd  20000  dmdprdsplitlem  20003  dmdprdsplit2lem  20011  dpjidcl  20024  ablfac1b  20036  pgpfac1lem1  20040  gsummgp0  20286  isirred  20388  irredrmul  20396  ringelnzr  20489  c0rhm  20500  c0rnghm  20501  zrrnghm  20502  zrinitorngc  20608  zrtermorngc  20609  isdomn2  20677  isdomn4  20682  isdrng2  20709  drngmcl  20716  isdrngd  20731  isdrngdOLD  20733  imadrhmcl  20763  cntzsdrg  20768  lcomfsupp  20886  lbspropd  21083  lspsneq  21109  lsppratlem6  21139  lbsextlem2  21146  lbsextlem4  21148  cnsubrg  21396  xrs1mnd  21409  xrs10  21410  xrs1cmn  21411  psgnodpm  21557  zrhpsgnodpm  21561  evpmodpmf1o  21565  uvcresum  21762  frlmssuvc1  21763  frlmsslsp  21765  frlmup2  21768  lindfrn  21790  f1lindf  21791  lindfmm  21796  islindf4  21807  psrbaglesupp  21891  psrlidm  21929  psrridm  21930  mplsubglem  21966  mpllsslem  21967  mplsubrglem  21971  mplmonmul  22003  mplcoe1  22004  mplcoe5  22007  mplbas2  22009  evlslem3  22047  evlsvvvallem  22058  evlsvvvallem2  22059  evlsvvval  22060  mhpvscacl  22109  psdmul  22121  coe1tmmul2  22229  coe1tmmul  22230  dmatmul  22450  1marepvsma1  22536  mdetdiaglem  22551  mdetrlin  22555  mdetrsca  22556  mdetralt  22561  maducoeval2  22593  madugsum  22596  symgmatr01  22607  gsummatr01lem3  22610  gsummatr01lem4  22611  gsummatr01  22612  smadiadetlem0  22614  smadiadetlem1a  22616  cmpfi  23361  2ndcdisj2  23410  elptr2  23527  ptcnplem  23574  xkopt  23608  kqdisj  23685  fin1aufil  23885  ptcmplem2  24006  ptcmplem3  24007  ptcmplem4  24008  opnsubg  24061  lpbl  24456  blcld  24458  zcld  24767  recld2  24768  reconnlem1  24780  divcn  24823  iundisj  25503  mbfeqalem1  25596  itg1val2  25639  itg1ge0  25641  i1fmullem  25649  i1fadd  25650  itg1addlem4  25654  itg1mulc  25659  itg1lea  25667  itg1le  25668  mbfi1fseqlem4  25673  itg2uba  25698  itg2lea  25699  itg2eqa  25700  itg2splitlem  25703  itg2split  25704  itgeqa  25769  ellimc3  25834  dvaddbr  25893  dvmulbr  25894  dvcobr  25901  dvcjbr  25904  dvrec  25910  dvrecg  25928  dvcnvlem  25931  dvexp3  25933  dveflem  25934  tdeglem4  26013  deg1n0ima  26042  deg1mul3le  26070  ig1peu  26128  ply1termlem  26156  plypf1  26165  plyaddlem1  26166  plymullem1  26167  coeeulem  26177  coeidlem  26190  coeid3  26193  coefv0  26201  coemulhi  26207  coemulc  26208  dvply1  26238  fta1  26262  vieta1lem2  26265  elaa  26270  elqaalem2  26274  aannenlem2  26283  aaliou2  26294  tayl0  26315  dvtaylp  26323  taylthlem1  26326  taylthlem2  26327  pserdvlem2  26381  logbcl  26719  relogbreexp  26727  relogbcxp  26737  cxplogb  26738  dcubic  26798  rlimcnp  26917  jensen  26940  dmgmaddn0  26974  dmlogdmgm  26975  lgamgulmlem2  26981  igamz  26999  gamp1  27009  regamcl  27012  wilthlem2  27020  basellem3  27034  chpub  27171  logexprlim  27176  lgslem1  27248  lgslem4  27251  lgsvalmod  27267  lgsqr  27302  lgsqrmod  27303  lgsqrmodndvds  27304  gausslemma2dlem0b  27308  gausslemma2dlem0c  27309  gausslemma2dlem0i  27315  gausslemma2dlem1a  27316  gausslemma2dlem4  27320  gausslemma2dlem5a  27321  gausslemma2dlem7  27324  gausslemma2d  27325  lgsquad2  27337  m1lgs  27339  2lgsoddprm  27367  2sqreultblem  27399  dchrisum0fno1  27462  rplogsum  27478  ishpg  28815  elntg2  29042  umgrislfupgrlem  29179  usgruspgrb  29240  nbumgrvtx  29403  nbupgrres  29421  isuvtx  29452  cusgrexilem2  29499  cusgrexi  29500  structtocusgr  29503  cusgrres  29505  cusgrfilem2  29513  vtxdginducedm1  29600  cusconngr  30249  2pthfrgr  30342  frgrncvvdeq  30367  frgrwopreglem4  30373  frgrwopreglem5  30379  frgrwopreg  30381  frgrhash2wsp  30390  strlem1  32309  strlem3  32312  strlem4  32313  strlem5  32314  hstrlem3  32320  hstrlem4  32321  iundisjf  32647  suppss3  32784  iundisjfi  32857  suppssnn0  32866  qsdrngi  33543  zringidom  33599  zringfrac  33602  psrmonmul  33682  irngnzply1  33823  qtophaus  33968  elzdif0  34112  measvunilem  34344  sibfof  34472  eulerpartlemb  34500  eulerpartlemf  34502  sseqf  34524  ballotlem5  34632  ballotlemi1  34635  ballotlemii  34636  ballotlemic  34639  ballotlem1c  34640  ballotlemscr  34651  ballotlemro  34655  ballotlemfg  34658  ballotlemfrc  34659  ballotlemfrceq  34661  ballotlemrinv0  34665  plymulx0  34679  signstfvn  34701  signsvfn  34714  bnj923  34899  bnj570  35035  bnj594  35042  fineqvnttrclselem1  35253  fineqvnttrclselem2  35254  fineqvnttrclselem3  35255  fineqvnttrclse  35256  subfacp1lem1  35349  satffunlem2lem1  35574  mrsubcn  35689  mrsubco  35691  circum  35844  dfon2lem6  35956  neibastop1  36529  bj-restn0b  37391  lindsadd  37922  lindsenlbs  37924  matunitlindflem1  37925  poimirlem24  37953  poimirlem25  37954  dvtan  37979  itg2addnclem2  37981  ftc1cnnc  38001  dvasin  38013  dvreasin  38015  dvreacos  38016  isdrngo2  38267  isdrngo3  38268  divrngidl  38337  isfldidl  38377  pridlc2  38381  pridlc3  38382  blockadjliftmap  38767  prter2  39315  lsateln0  39429  lsatlss  39430  lsmsat  39442  lsatcv0  39465  lsat0cv  39467  lcv1  39475  l1cvpat  39488  dih1dimatlem  41763  dihatexv2  41773  djhcvat42  41849  dihjat1lem  41862  dochsatshp  41885  lcfl6  41934  mapdrvallem2  42079  mapdpglem32  42139  idomnnzgmulnz  42560  aks6d1c5lem3  42564  aks6d1c5lem2  42565  deg1gprod  42567  sticksstones22  42595  unitscyglem4  42625  readvrec2  42781  readvrec  42782  readvcot  42784  evlsbagval  42990  selvvvval  43006  evlselv  43008  evlsmhpvvval  43016  prjspertr  43026  prjsperref  43027  prjspersym  43028  prjspvs  43031  prjsprellsp  43032  dffltz  43055  irrapx1  43244  pell1234qrne0  43269  pell1234qrreccl  43270  pell1234qrmulcl  43271  pell14qrgt0  43275  pell1234qrdich  43277  pell14qrdich  43285  pell1qrge1  43286  pell1qr1  43287  pell1qrgap  43290  pell14qrgapw  43292  pellqrexplicit  43293  pellqrex  43295  pellfundge  43298  pellfundgt1  43299  setindtr  43440  kelac1  43479  mpaaeu  43566  flcidc  43586  deg1mhm  43616  onexoegt  43660  cantnfub  43737  cantnfresb  43740  succlg  43744  dflim5  43745  onmcl  43747  omabs2  43748  tfsconcatrev  43764  minregex2  43950  radcnvrat  44729  binomcxplemdvbinom  44768  disjiun2  45477  fiiuncl  45484  disjf1o  45609  difmapsn  45629  supminfxr2  45885  icoiccdif  45942  iccdificc  45957  fsumnncl  45990  fsumsupp0  45996  fprod0  46014  climrec  46021  islpcn  46055  lptre2pt  46056  limclner  46067  cnrefiisplem  46245  fprodcncf  46316  fperdvper  46335  dvdivcncf  46343  dvnmul  46359  dvmptfprodlem  46360  dvnprodlem2  46363  stoweidlem25  46441  stoweidlem28  46444  stoweidlem41  46457  stoweidlem44  46460  stoweidlem46  46462  stirlinglem5  46494  dirkercncflem1  46519  dirkercncflem2  46520  fourierdlem24  46547  fourierdlem62  46584  fouriersw  46647  fouriercn  46648  elaa2lem  46649  elaa2  46650  etransclem25  46675  etransclem35  46685  etransclem44  46694  sge0iunmptlemfi  46829  sge0fodjrnlem  46832  iundjiunlem  46875  meadjiunlem  46881  meaiininclem  46902  isomenndlem  46946  hsphoidmvle2  47001  hsphoidmvle  47002  hoidmv1lelem2  47008  hoidmvle  47016  ovnhoilem1  47017  hspdifhsp  47032  hspmbllem2  47043  ovnsubadd2lem  47061  ovolval4lem1  47065  preimagelt  47115  preimalegt  47116  chnsubseq  47298  fsummsndifre  47816  fsummmodsndifre  47818  odz2prm2pw  48014  fmtnoprmfac1lem  48015  fmtnoprmfac2lem1  48017  2pwp1prm  48040  lighneallem2  48057  lighneallem3  48058  lighneallem4  48061  bgoldbtbndlem2  48270  bgoldbtbndlem3  48271  bgoldbtbndlem4  48272  bgoldbtbnd  48273  isubgrvtxuhgr  48328  2zrngnmlid2  48721  mgpsumunsn  48825  mgpsumz  48826  mgpsumn  48827  lindslinindsimp1  48921  lindslinindsimp2  48927  lincresunit1  48941  lincresunit2  48942  lincresunit3lem1  48943  lincresunit3lem2  48944  lincresunit3  48945  lindssnlvec  48950  logcxp0  48999  relogbmulbexp  49025  relogbdivb  49026  dignn0fr  49065  rrxlinesc  49199  eenglngeehlnmlem1  49201  eenglngeehlnmlem2  49202