Theorem eldifi 4154

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2108   ∖ cdif 3973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979

This theorem is referenced by:  difss  4159  eqoreldif  4708  xpdifid  6199  tz7.7  6421  tfi  7890  peano5  7932  peano5OLD  7933  xpord2pred  8186  frrlem12  8338  frrlem13  8339  wfrlem10OLD  8374  wfrlem15OLD  8379  tz7.48-1  8499  tz7.49  8501  dif20el  8561  oaf1o  8619  oeordi  8643  oeord  8644  oecan  8645  oeword  8646  oeworde  8649  oelimcl  8656  oeeulem  8657  oeeui  8658  oaabs2  8705  boxcutc  8999  domdifsn  9120  pssnn  9234  isinf  9323  isinfOLD  9324  pwfilem  9384  pwfilemOLD  9416  fsuppco2  9472  fsuppcor  9473  ordtypelem7  9593  unxpwdom2  9657  inf3lem3  9699  cantnfp1lem1  9747  cantnfp1lem3  9749  ttrcltr  9785  infxpenc2lem1  10088  dfacacn  10211  isf32lem3  10424  isf34lem4  10446  fin67  10464  isfin7-2  10465  domtriomlem  10511  axdc2lem  10517  axdc3lem4  10522  axdc4lem  10524  ttukeylem7  10584  konigthlem  10637  fpwwe2lem12  10711  fpwwe2  10712  modfzo0difsn  13994  hashf1lem1  14504  hashle2prv  14527  rlimrege0  15625  rlimrecl  15626  sumrblem  15759  fsumcvg  15760  summolem2a  15763  fsumss  15773  fsumsplit1  15793  fsumless  15844  cvgcmpce  15866  binomlem  15877  incexclem  15884  incexc  15885  isumltss  15896  prodrblem  15977  fprodcvg  15978  prodmolem2a  15982  fprodss  15996  fprodn0f  16039  fprodeq0g  16042  fprodmodd  16045  rpnnen2lem10  16271  rpnnen2lem11  16272  sumeven  16435  sumodd  16436  lcmfunsnlem2  16687  oddprmge3  16747  oddprm  16857  nnoddn2prm  16858  nnoddn2prmb  16860  iserodd  16882  prmreclem2  16964  prmreclem3  16965  prmreclem5  16967  4sqlem19  17010  prmdvdsprmo  17089  prmodvdslcmf  17094  prmlem0  17153  firest  17492  grpinvnzcl  19051  symgextfv  19460  pmtrf  19497  pmtrdifellem3  19520  sylow2alem2  19660  sylow2a  19661  efgsf  19771  efgsrel  19776  efgs1  19777  efgsfo  19781  gsumzaddlem  19963  gsumzadd  19964  gsumzmhm  19979  gsum2d2lem  20015  dprdfadd  20064  dprdres  20072  subgdmdprd  20078  dmdprdsplitlem  20081  dmdprdsplit2lem  20089  dpjidcl  20102  ablfac1b  20114  pgpfac1lem1  20118  gsummgp0  20341  isirred  20445  irredrmul  20453  ringelnzr  20549  c0rhm  20560  c0rnghm  20561  zrrnghm  20562  zrinitorngc  20664  zrtermorngc  20665  isdomn2  20733  isdomn4  20738  isdrng2  20765  drngmcl  20772  isdrngd  20787  isdrngdOLD  20789  imadrhmcl  20820  cntzsdrg  20825  lcomfsupp  20922  lbspropd  21121  lspsneq  21147  lsppratlem6  21177  lbsextlem2  21184  lbsextlem4  21186  xrs1mnd  21445  xrs10  21446  xrs1cmn  21447  cnsubrg  21468  psgnodpm  21629  zrhpsgnodpm  21633  evpmodpmf1o  21637  uvcresum  21836  frlmssuvc1  21837  frlmsslsp  21839  frlmup2  21842  lindfrn  21864  f1lindf  21865  lindfmm  21870  islindf4  21881  psrbaglesupp  21965  psrlidm  22005  psrridm  22006  mplsubglem  22042  mpllsslem  22043  mplsubrglem  22047  mplmonmul  22077  mplcoe1  22078  mplcoe5  22081  mplbas2  22083  evlslem3  22127  mhpvscacl  22181  psdmul  22193  coe1tmmul2  22300  coe1tmmul  22301  dmatmul  22524  1marepvsma1  22610  mdetdiaglem  22625  mdetrlin  22629  mdetrsca  22630  mdetralt  22635  maducoeval2  22667  madugsum  22670  symgmatr01  22681  gsummatr01lem3  22684  gsummatr01lem4  22685  gsummatr01  22686  smadiadetlem0  22688  smadiadetlem1a  22690  cmpfi  23437  2ndcdisj2  23486  elptr2  23603  ptcnplem  23650  xkopt  23684  kqdisj  23761  fin1aufil  23961  ptcmplem2  24082  ptcmplem3  24083  ptcmplem4  24084  opnsubg  24137  lpbl  24537  blcld  24539  zcld  24854  recld2  24855  reconnlem1  24867  divcnOLD  24909  divcn  24911  iundisj  25602  mbfeqalem1  25695  itg1val2  25738  itg1ge0  25740  i1fmullem  25748  i1fadd  25749  itg1addlem4  25753  itg1addlem4OLD  25754  itg1mulc  25759  itg1lea  25767  itg1le  25768  mbfi1fseqlem4  25773  itg2uba  25798  itg2lea  25799  itg2eqa  25800  itg2splitlem  25803  itg2split  25804  itgeqa  25869  ellimc3  25934  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcobr  26003  dvcobrOLD  26004  dvcjbr  26007  dvrec  26013  dvrecg  26031  dvcnvlem  26034  dvexp3  26036  dveflem  26037  tdeglem4  26119  deg1n0ima  26148  deg1mul3le  26176  ig1peu  26234  ply1termlem  26262  plypf1  26271  plyaddlem1  26272  plymullem1  26273  coeeulem  26283  coeidlem  26296  coeid3  26299  coefv0  26307  coemulhi  26313  coemulc  26314  dvply1  26343  fta1  26368  vieta1lem2  26371  elaa  26376  elqaalem2  26380  aannenlem2  26389  aaliou2  26400  tayl0  26421  dvtaylp  26430  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  pserdvlem2  26490  logbcl  26828  relogbreexp  26836  relogbcxp  26846  cxplogb  26847  dcubic  26907  rlimcnp  27026  jensen  27050  dmgmaddn0  27084  dmlogdmgm  27085  lgamgulmlem2  27091  igamz  27109  gamp1  27119  regamcl  27122  wilthlem2  27130  basellem3  27144  chpub  27282  logexprlim  27287  lgslem1  27359  lgslem4  27362  lgsvalmod  27378  lgsqr  27413  lgsqrmod  27414  lgsqrmodndvds  27415  gausslemma2dlem0b  27419  gausslemma2dlem0c  27420  gausslemma2dlem0i  27426  gausslemma2dlem1a  27427  gausslemma2dlem4  27431  gausslemma2dlem5a  27432  gausslemma2dlem7  27435  gausslemma2d  27436  lgsquad2  27448  m1lgs  27450  2lgsoddprm  27478  2sqreultblem  27510  dchrisum0fno1  27573  rplogsum  27589  ishpg  28785  elntg2  29018  umgrislfupgrlem  29157  usgruspgrb  29218  nbumgrvtx  29381  nbupgrres  29399  isuvtx  29430  cusgrexilem2  29477  cusgrexi  29478  structtocusgr  29481  cusgrres  29484  cusgrfilem2  29492  vtxdginducedm1  29579  cusconngr  30223  2pthfrgr  30316  frgrncvvdeq  30341  frgrwopreglem4  30347  frgrwopreglem5  30353  frgrwopreg  30355  frgrhash2wsp  30364  strlem1  32282  strlem3  32285  strlem4  32286  strlem5  32287  hstrlem3  32293  hstrlem4  32294  iundisjf  32611  suppss3  32738  iundisjfi  32801  suppssnn0  32812  qsdrngi  33488  zringidom  33544  zringfrac  33547  irngnzply1  33691  qtophaus  33782  elzdif0  33926  ind0  33982  measvunilem  34176  sibfof  34305  eulerpartlemb  34333  eulerpartlemf  34335  sseqf  34357  ballotlem5  34464  ballotlemi1  34467  ballotlemii  34468  ballotlemic  34471  ballotlem1c  34472  ballotlemscr  34483  ballotlemro  34487  ballotlemfg  34490  ballotlemfrc  34491  ballotlemfrceq  34493  ballotlemrinv0  34497  plymulx0  34524  signstfvn  34546  signsvfn  34559  bnj923  34744  bnj570  34881  bnj594  34888  subfacp1lem1  35147  satffunlem2lem1  35372  mrsubcn  35487  mrsubco  35489  circum  35642  dfon2lem6  35752  neibastop1  36325  bj-restn0b  37057  lindsadd  37573  lindsenlbs  37575  matunitlindflem1  37576  poimirlem24  37604  poimirlem25  37605  dvtan  37630  itg2addnclem2  37632  ftc1cnnc  37652  dvasin  37664  dvreasin  37666  dvreacos  37667  isdrngo2  37918  isdrngo3  37919  divrngidl  37988  isfldidl  38028  pridlc2  38032  pridlc3  38033  prter2  38837  lsateln0  38951  lsatlss  38952  lsmsat  38964  lsatcv0  38987  lsat0cv  38989  lcv1  38997  l1cvpat  39010  dih1dimatlem  41286  dihatexv2  41296  djhcvat42  41372  dihjat1lem  41385  dochsatshp  41408  lcfl6  41457  mapdrvallem2  41602  mapdpglem32  41662  idomnnzgmulnz  42090  aks6d1c5lem3  42094  aks6d1c5lem2  42095  deg1gprod  42097  sticksstones22  42125  unitscyglem4  42155  evlsvvvallem  42516  evlsvvvallem2  42517  evlsvvval  42518  evlsbagval  42521  selvvvval  42540  evlselv  42542  evlsmhpvvval  42550  prjspertr  42560  prjsperref  42561  prjspersym  42562  prjspvs  42565  prjsprellsp  42566  dffltz  42589  irrapx1  42784  pell1234qrne0  42809  pell1234qrreccl  42810  pell1234qrmulcl  42811  pell14qrgt0  42815  pell1234qrdich  42817  pell14qrdich  42825  pell1qrge1  42826  pell1qr1  42827  pell1qrgap  42830  pell14qrgapw  42832  pellqrexplicit  42833  pellqrex  42835  pellfundge  42838  pellfundgt1  42839  setindtr  42981  kelac1  43020  mpaaeu  43107  flcidc  43131  deg1mhm  43161  onexoegt  43205  cantnfub  43283  cantnfresb  43286  succlg  43290  dflim5  43291  onmcl  43293  omabs2  43294  tfsconcatrev  43310  minregex2  43497  radcnvrat  44283  binomcxplemdvbinom  44322  disjiun2  44960  fiiuncl  44967  disjf1o  45098  difmapsn  45119  supminfxr2  45384  icoiccdif  45442  iccdificc  45457  fsumnncl  45493  fsumsupp0  45499  fprod0  45517  climrec  45524  islpcn  45560  lptre2pt  45561  limclner  45572  cnrefiisplem  45750  fprodcncf  45821  fperdvper  45840  dvdivcncf  45848  dvnmul  45864  dvmptfprodlem  45865  dvnprodlem2  45868  stoweidlem25  45946  stoweidlem28  45949  stoweidlem41  45962  stoweidlem44  45965  stoweidlem46  45967  stirlinglem5  45999  dirkercncflem1  46024  dirkercncflem2  46025  fourierdlem24  46052  fourierdlem62  46089  fouriersw  46152  fouriercn  46153  elaa2lem  46154  elaa2  46155  etransclem25  46180  etransclem35  46190  etransclem44  46199  sge0iunmptlemfi  46334  sge0fodjrnlem  46337  iundjiunlem  46380  meadjiunlem  46386  meaiininclem  46407  isomenndlem  46451  hsphoidmvle2  46506  hsphoidmvle  46507  hoidmv1lelem2  46513  hoidmvle  46521  ovnhoilem1  46522  hspdifhsp  46537  hspmbllem2  46548  ovnsubadd2lem  46566  ovolval4lem1  46570  preimagelt  46620  preimalegt  46621  fsummsndifre  47246  fsummmodsndifre  47248  odz2prm2pw  47437  fmtnoprmfac1lem  47438  fmtnoprmfac2lem1  47440  2pwp1prm  47463  lighneallem2  47480  lighneallem3  47481  lighneallem4  47484  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbndlem4  47682  bgoldbtbnd  47683  isubgrvtxuhgr  47736  2zrngnmlid2  47980  mgpsumunsn  48086  mgpsumz  48087  mgpsumn  48088  lindslinindsimp1  48186  lindslinindsimp2  48192  lincresunit1  48206  lincresunit2  48207  lincresunit3lem1  48208  lincresunit3lem2  48209  lincresunit3  48210  lindssnlvec  48215  logcxp0  48269  relogbmulbexp  48295  relogbdivb  48296  dignn0fr  48335  rrxlinesc  48469  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472