Theorem eldifi 4127

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

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

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 3952

This theorem is referenced by:  difss  4132  eqoreldif  4689  xpdifid  6168  tz7.7  6391  tfi  7842  peano5  7884  peano5OLD  7885  xpord2pred  8131  frrlem12  8282  frrlem13  8283  wfrlem10OLD  8318  wfrlem15OLD  8323  tz7.48-1  8443  tz7.49  8445  dif20el  8505  oaf1o  8563  oeordi  8587  oeord  8588  oecan  8589  oeword  8590  oeworde  8593  oelimcl  8600  oeeulem  8601  oeeui  8602  oaabs2  8648  boxcutc  8935  domdifsn  9054  pssnn  9168  pwfilem  9177  isinf  9260  isinfOLD  9261  pssnnOLD  9265  pwfilemOLD  9346  fsuppco2  9398  fsuppcor  9399  ordtypelem7  9519  unxpwdom2  9583  inf3lem3  9625  cantnfp1lem1  9673  cantnfp1lem3  9675  ttrcltr  9711  infxpenc2lem1  10014  dfacacn  10136  isf32lem3  10350  isf34lem4  10372  fin67  10390  isfin7-2  10391  domtriomlem  10437  axdc2lem  10443  axdc3lem4  10448  axdc4lem  10450  ttukeylem7  10510  konigthlem  10563  fpwwe2lem12  10637  fpwwe2  10638  modfzo0difsn  13908  hashf1lem1  14415  hashf1lem1OLD  14416  hashle2prv  14439  rlimrege0  15523  rlimrecl  15524  sumrblem  15657  fsumcvg  15658  summolem2a  15661  fsumss  15671  fsumsplit1  15691  fsumless  15742  cvgcmpce  15764  binomlem  15775  incexclem  15782  incexc  15783  isumltss  15794  prodrblem  15873  fprodcvg  15874  prodmolem2a  15878  fprodss  15892  fprodn0f  15935  fprodeq0g  15938  fprodmodd  15941  rpnnen2lem10  16166  rpnnen2lem11  16167  sumeven  16330  sumodd  16331  lcmfunsnlem2  16577  oddprmge3  16637  oddprm  16743  nnoddn2prm  16744  nnoddn2prmb  16746  iserodd  16768  prmreclem2  16850  prmreclem3  16851  prmreclem5  16853  4sqlem19  16896  prmdvdsprmo  16975  prmodvdslcmf  16980  prmlem0  17039  firest  17378  grpinvnzcl  18895  symgextfv  19286  pmtrf  19323  pmtrdifellem3  19346  sylow2alem2  19486  sylow2a  19487  efgsf  19597  efgsrel  19602  efgs1  19603  efgsfo  19607  gsumzaddlem  19789  gsumzadd  19790  gsumzmhm  19805  gsum2d2lem  19841  dprdfadd  19890  dprdres  19898  subgdmdprd  19904  dmdprdsplitlem  19907  dmdprdsplit2lem  19915  dpjidcl  19928  ablfac1b  19940  pgpfac1lem1  19944  gsummgp0  20130  isirred  20233  irredrmul  20241  ringelnzr  20300  isdrng2  20371  isdrngd  20390  isdrngdOLD  20392  imadrhmcl  20413  cntzsdrg  20418  lcomfsupp  20512  lbspropd  20710  lspsneq  20735  lsppratlem6  20765  lbsextlem2  20772  lbsextlem4  20774  isdomn4  20918  xrs1mnd  20983  xrs10  20984  xrs1cmn  20985  cnsubrg  21005  psgnodpm  21141  zrhpsgnodpm  21145  evpmodpmf1o  21149  uvcresum  21348  frlmssuvc1  21349  frlmsslsp  21351  frlmup2  21354  lindfrn  21376  f1lindf  21377  lindfmm  21382  islindf4  21393  psrbaglesupp  21477  psrbaglesuppOLD  21478  psrlidm  21523  psrridm  21524  mplsubglem  21558  mpllsslem  21559  mplsubrglem  21563  mplmonmul  21591  mplcoe1  21592  mplcoe5  21595  mplbas2  21597  evlslem3  21643  mhpvscacl  21697  coe1tmmul2  21798  coe1tmmul  21799  dmatmul  21999  1marepvsma1  22085  mdetdiaglem  22100  mdetrlin  22104  mdetrsca  22105  mdetralt  22110  maducoeval2  22142  madugsum  22145  symgmatr01  22156  gsummatr01lem3  22159  gsummatr01lem4  22160  gsummatr01  22161  smadiadetlem0  22163  smadiadetlem1a  22165  cmpfi  22912  2ndcdisj2  22961  elptr2  23078  ptcnplem  23125  xkopt  23159  kqdisj  23236  fin1aufil  23436  ptcmplem2  23557  ptcmplem3  23558  ptcmplem4  23559  opnsubg  23612  lpbl  24012  blcld  24014  zcld  24329  recld2  24330  reconnlem1  24342  divcn  24384  iundisj  25065  mbfeqalem1  25158  itg1val2  25201  itg1ge0  25203  i1fmullem  25211  i1fadd  25212  itg1addlem4  25216  itg1addlem4OLD  25217  itg1mulc  25222  itg1lea  25230  itg1le  25231  mbfi1fseqlem4  25236  itg2uba  25261  itg2lea  25262  itg2eqa  25263  itg2splitlem  25266  itg2split  25267  itgeqa  25331  ellimc3  25396  dvaddbr  25455  dvmulbr  25456  dvcobr  25463  dvcjbr  25466  dvrec  25472  dvrecg  25490  dvcnvlem  25493  dvexp3  25495  dveflem  25496  tdeglem4  25577  tdeglem4OLD  25578  deg1n0ima  25607  deg1mul3le  25634  ig1peu  25689  ply1termlem  25717  plypf1  25726  plyaddlem1  25727  plymullem1  25728  coeeulem  25738  coeidlem  25751  coeid3  25754  coefv0  25762  coemulhi  25768  coemulc  25769  dvply1  25797  fta1  25821  vieta1lem2  25824  elaa  25829  elqaalem2  25833  aannenlem2  25842  aaliou2  25853  tayl0  25874  dvtaylp  25882  taylthlem1  25885  taylthlem2  25886  pserdvlem2  25940  logbcl  26272  relogbreexp  26280  relogbcxp  26290  cxplogb  26291  dcubic  26351  rlimcnp  26470  jensen  26493  dmgmaddn0  26527  dmlogdmgm  26528  lgamgulmlem2  26534  igamz  26552  gamp1  26562  regamcl  26565  wilthlem2  26573  basellem3  26587  chpub  26723  logexprlim  26728  lgslem1  26800  lgslem4  26803  lgsvalmod  26819  lgsqr  26854  lgsqrmod  26855  lgsqrmodndvds  26856  gausslemma2dlem0b  26860  gausslemma2dlem0c  26861  gausslemma2dlem0i  26867  gausslemma2dlem1a  26868  gausslemma2dlem4  26872  gausslemma2dlem5a  26873  gausslemma2dlem7  26876  gausslemma2d  26877  lgsquad2  26889  m1lgs  26891  2lgsoddprm  26919  2sqreultblem  26951  dchrisum0fno1  27014  rplogsum  27030  ishpg  28041  elntg2  28274  umgrislfupgrlem  28413  usgruspgrb  28472  nbumgrvtx  28634  nbupgrres  28652  isuvtx  28683  cusgrexilem2  28730  cusgrexi  28731  structtocusgr  28734  cusgrres  28736  cusgrfilem2  28744  vtxdginducedm1  28831  cusconngr  29475  2pthfrgr  29568  frgrncvvdeq  29593  frgrwopreglem4  29599  frgrwopreglem5  29605  frgrwopreg  29607  frgrhash2wsp  29616  strlem1  31534  strlem3  31537  strlem4  31538  strlem5  31539  hstrlem3  31545  hstrlem4  31546  iundisjf  31851  suppss3  31980  iundisjfi  32038  suppssnn0  32048  qsdrngi  32640  irngnzply1  32786  qtophaus  32847  elzdif0  32991  ind0  33047  measvunilem  33241  sibfof  33370  eulerpartlemb  33398  eulerpartlemf  33400  sseqf  33422  ballotlem5  33529  ballotlemi1  33532  ballotlemii  33533  ballotlemic  33536  ballotlem1c  33537  ballotlemscr  33548  ballotlemro  33552  ballotlemfg  33555  ballotlemfrc  33556  ballotlemfrceq  33558  ballotlemrinv0  33562  plymulx0  33589  signstfvn  33611  signsvfn  33624  bnj923  33810  bnj570  33947  bnj594  33954  subfacp1lem1  34201  satffunlem2lem1  34426  mrsubcn  34541  mrsubco  34543  circum  34690  dfon2lem6  34791  gg-divcn  35194  gg-dvmulbr  35206  gg-dvcobr  35207  neibastop1  35292  bj-restn0b  36020  lindsadd  36529  lindsenlbs  36531  matunitlindflem1  36532  poimirlem24  36560  poimirlem25  36561  dvtan  36586  itg2addnclem2  36588  ftc1cnnc  36608  dvasin  36620  dvreasin  36622  dvreacos  36623  isdrngo2  36874  isdrngo3  36875  divrngidl  36944  isfldidl  36984  pridlc2  36988  pridlc3  36989  prter2  37799  lsateln0  37913  lsatlss  37914  lsmsat  37926  lsatcv0  37949  lsat0cv  37951  lcv1  37959  l1cvpat  37972  dih1dimatlem  40248  dihatexv2  40258  djhcvat42  40334  dihjat1lem  40347  dochsatshp  40370  lcfl6  40419  mapdrvallem2  40564  mapdpglem32  40624  sticksstones22  41032  evlsvvvallem  41181  evlsvvvallem2  41182  evlsvvval  41183  evlsbagval  41186  selvvvval  41205  evlselv  41207  evlsmhpvvval  41215  prjspertr  41395  prjsperref  41396  prjspersym  41397  prjspvs  41400  prjsprellsp  41401  dffltz  41424  irrapx1  41614  pell1234qrne0  41639  pell1234qrreccl  41640  pell1234qrmulcl  41641  pell14qrgt0  41645  pell1234qrdich  41647  pell14qrdich  41655  pell1qrge1  41656  pell1qr1  41657  pell1qrgap  41660  pell14qrgapw  41662  pellqrexplicit  41663  pellqrex  41665  pellfundge  41668  pellfundgt1  41669  setindtr  41811  kelac1  41853  mpaaeu  41940  flcidc  41964  deg1mhm  41997  onexoegt  42041  cantnfub  42119  cantnfresb  42122  succlg  42126  dflim5  42127  onmcl  42129  omabs2  42130  tfsconcatrev  42146  minregex2  42334  radcnvrat  43121  binomcxplemdvbinom  43160  disjiun2  43793  fiiuncl  43800  disjf1o  43937  difmapsn  43959  supminfxr2  44227  icoiccdif  44285  iccdificc  44300  fsumnncl  44336  fsumsupp0  44342  fprod0  44360  climrec  44367  islpcn  44403  lptre2pt  44404  limclner  44415  cnrefiisplem  44593  fprodcncf  44664  fperdvper  44683  dvdivcncf  44691  dvnmul  44707  dvmptfprodlem  44708  dvnprodlem2  44711  stoweidlem25  44789  stoweidlem28  44792  stoweidlem41  44805  stoweidlem44  44808  stoweidlem46  44810  stirlinglem5  44842  dirkercncflem1  44867  dirkercncflem2  44868  fourierdlem24  44895  fourierdlem62  44932  fouriersw  44995  fouriercn  44996  elaa2lem  44997  elaa2  44998  etransclem25  45023  etransclem35  45033  etransclem44  45042  sge0iunmptlemfi  45177  sge0fodjrnlem  45180  iundjiunlem  45223  meadjiunlem  45229  meaiininclem  45250  isomenndlem  45294  hsphoidmvle2  45349  hsphoidmvle  45350  hoidmv1lelem2  45356  hoidmvle  45364  ovnhoilem1  45365  hspdifhsp  45380  hspmbllem2  45391  ovnsubadd2lem  45409  ovolval4lem1  45413  preimagelt  45463  preimalegt  45464  fsummsndifre  46088  fsummmodsndifre  46090  odz2prm2pw  46279  fmtnoprmfac1lem  46280  fmtnoprmfac2lem1  46282  2pwp1prm  46305  lighneallem2  46322  lighneallem3  46323  lighneallem4  46326  bgoldbtbndlem2  46522  bgoldbtbndlem3  46523  bgoldbtbndlem4  46524  bgoldbtbnd  46525  c0rhm  46759  c0rnghm  46760  zrrnghm  46764  2zrngnmlid2  46897  zrinitorngc  46946  zrtermorngc  46947  mgpsumunsn  47085  mgpsumz  47086  mgpsumn  47087  lindslinindsimp1  47186  lindslinindsimp2  47192  lincresunit1  47206  lincresunit2  47207  lincresunit3lem1  47208  lincresunit3lem2  47209  lincresunit3  47210  lindssnlvec  47215  logcxp0  47269  relogbmulbexp  47295  relogbdivb  47296  dignn0fr  47335  rrxlinesc  47469  eenglngeehlnmlem1  47471  eenglngeehlnmlem2  47472