Theorem eldifi 4090

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   ∖ cdif 3908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914

This theorem is referenced by:  difss  4095  eqoreldif  4645  xpdifid  6130  tz7.7  6347  tfi  7810  peano5  7850  resf1extb  7891  resf1ext2b  7892  xpord2pred  8102  frrlem12  8254  frrlem13  8255  tz7.48-1  8389  tz7.49  8391  dif20el  8447  oaf1o  8505  oeordi  8529  oeord  8530  oecan  8531  oeword  8532  oeworde  8535  oelimcl  8542  oeeulem  8543  oeeui  8544  oaabs2  8591  boxcutc  8892  domdifsn  9002  pssnn  9110  isinf  9184  isinfOLD  9185  pwfilem  9244  fsuppco2  9331  fsuppcor  9332  ordtypelem7  9454  unxpwdom2  9518  inf3lem3  9562  cantnfp1lem1  9610  cantnfp1lem3  9612  ttrcltr  9648  infxpenc2lem1  9951  dfacacn  10074  isf32lem3  10287  isf34lem4  10309  fin67  10327  isfin7-2  10328  domtriomlem  10374  axdc2lem  10380  axdc3lem4  10385  axdc4lem  10387  ttukeylem7  10447  konigthlem  10500  fpwwe2lem12  10574  fpwwe2  10575  modfzo0difsn  13887  hashf1lem1  14399  hashle2prv  14422  rlimrege0  15523  rlimrecl  15524  sumrblem  15655  fsumcvg  15656  summolem2a  15659  fsumss  15669  fsumsplit1  15689  fsumless  15740  cvgcmpce  15762  binomlem  15773  incexclem  15780  incexc  15781  isumltss  15792  prodrblem  15873  fprodcvg  15874  prodmolem2a  15878  fprodss  15892  fprodn0f  15935  fprodeq0g  15938  fprodmodd  15941  rpnnen2lem10  16169  rpnnen2lem11  16170  sumeven  16335  sumodd  16336  lcmfunsnlem2  16588  oddprmge3  16648  oddprm  16759  nnoddn2prm  16760  nnoddn2prmb  16762  iserodd  16784  prmreclem2  16866  prmreclem3  16867  prmreclem5  16869  4sqlem19  16912  prmdvdsprmo  16991  prmodvdslcmf  16996  prmlem0  17054  firest  17373  grpinvnzcl  18927  symgextfv  19334  pmtrf  19371  pmtrdifellem3  19394  sylow2alem2  19534  sylow2a  19535  efgsf  19645  efgsrel  19650  efgs1  19651  efgsfo  19655  gsumzaddlem  19837  gsumzadd  19838  gsumzmhm  19853  gsum2d2lem  19889  dprdfadd  19938  dprdres  19946  subgdmdprd  19952  dmdprdsplitlem  19955  dmdprdsplit2lem  19963  dpjidcl  19976  ablfac1b  19988  pgpfac1lem1  19992  gsummgp0  20240  isirred  20341  irredrmul  20349  ringelnzr  20445  c0rhm  20456  c0rnghm  20457  zrrnghm  20458  zrinitorngc  20564  zrtermorngc  20565  isdomn2  20633  isdomn4  20638  isdrng2  20665  drngmcl  20672  isdrngd  20687  isdrngdOLD  20689  imadrhmcl  20719  cntzsdrg  20724  lcomfsupp  20842  lbspropd  21040  lspsneq  21066  lsppratlem6  21096  lbsextlem2  21103  lbsextlem4  21105  cnsubrg  21371  xrs1mnd  21384  xrs10  21385  xrs1cmn  21386  psgnodpm  21532  zrhpsgnodpm  21536  evpmodpmf1o  21540  uvcresum  21737  frlmssuvc1  21738  frlmsslsp  21740  frlmup2  21743  lindfrn  21765  f1lindf  21766  lindfmm  21771  islindf4  21782  psrbaglesupp  21866  psrlidm  21906  psrridm  21907  mplsubglem  21943  mpllsslem  21944  mplsubrglem  21948  mplmonmul  21978  mplcoe1  21979  mplcoe5  21982  mplbas2  21984  evlslem3  22022  mhpvscacl  22076  psdmul  22088  coe1tmmul2  22197  coe1tmmul  22198  dmatmul  22419  1marepvsma1  22505  mdetdiaglem  22520  mdetrlin  22524  mdetrsca  22525  mdetralt  22530  maducoeval2  22562  madugsum  22565  symgmatr01  22576  gsummatr01lem3  22579  gsummatr01lem4  22580  gsummatr01  22581  smadiadetlem0  22583  smadiadetlem1a  22585  cmpfi  23330  2ndcdisj2  23379  elptr2  23496  ptcnplem  23543  xkopt  23577  kqdisj  23654  fin1aufil  23854  ptcmplem2  23975  ptcmplem3  23976  ptcmplem4  23977  opnsubg  24030  lpbl  24426  blcld  24428  zcld  24737  recld2  24738  reconnlem1  24750  divcnOLD  24792  divcn  24794  iundisj  25484  mbfeqalem1  25577  itg1val2  25620  itg1ge0  25622  i1fmullem  25630  i1fadd  25631  itg1addlem4  25635  itg1mulc  25640  itg1lea  25648  itg1le  25649  mbfi1fseqlem4  25654  itg2uba  25679  itg2lea  25680  itg2eqa  25681  itg2splitlem  25684  itg2split  25685  itgeqa  25750  ellimc3  25815  dvaddbr  25875  dvmulbr  25876  dvmulbrOLD  25877  dvcobr  25884  dvcobrOLD  25885  dvcjbr  25888  dvrec  25894  dvrecg  25912  dvcnvlem  25915  dvexp3  25917  dveflem  25918  tdeglem4  26000  deg1n0ima  26029  deg1mul3le  26057  ig1peu  26115  ply1termlem  26143  plypf1  26152  plyaddlem1  26153  plymullem1  26154  coeeulem  26164  coeidlem  26177  coeid3  26180  coefv0  26188  coemulhi  26194  coemulc  26195  dvply1  26226  fta1  26251  vieta1lem2  26254  elaa  26259  elqaalem2  26263  aannenlem2  26272  aaliou2  26283  tayl0  26304  dvtaylp  26313  taylthlem1  26316  taylthlem2  26317  taylthlem2OLD  26318  pserdvlem2  26373  logbcl  26712  relogbreexp  26720  relogbcxp  26730  cxplogb  26731  dcubic  26791  rlimcnp  26910  jensen  26934  dmgmaddn0  26968  dmlogdmgm  26969  lgamgulmlem2  26975  igamz  26993  gamp1  27003  regamcl  27006  wilthlem2  27014  basellem3  27028  chpub  27166  logexprlim  27171  lgslem1  27243  lgslem4  27246  lgsvalmod  27262  lgsqr  27297  lgsqrmod  27298  lgsqrmodndvds  27299  gausslemma2dlem0b  27303  gausslemma2dlem0c  27304  gausslemma2dlem0i  27310  gausslemma2dlem1a  27311  gausslemma2dlem4  27315  gausslemma2dlem5a  27316  gausslemma2dlem7  27319  gausslemma2d  27320  lgsquad2  27332  m1lgs  27334  2lgsoddprm  27362  2sqreultblem  27394  dchrisum0fno1  27457  rplogsum  27473  ishpg  28741  elntg2  28967  umgrislfupgrlem  29104  usgruspgrb  29165  nbumgrvtx  29328  nbupgrres  29346  isuvtx  29377  cusgrexilem2  29424  cusgrexi  29425  structtocusgr  29428  cusgrres  29431  cusgrfilem2  29439  vtxdginducedm1  29526  cusconngr  30172  2pthfrgr  30265  frgrncvvdeq  30290  frgrwopreglem4  30296  frgrwopreglem5  30302  frgrwopreg  30304  frgrhash2wsp  30313  strlem1  32231  strlem3  32234  strlem4  32235  strlem5  32236  hstrlem3  32242  hstrlem4  32243  iundisjf  32570  suppss3  32699  iundisjfi  32771  suppssnn0  32782  ind0  32833  qsdrngi  33461  zringidom  33517  zringfrac  33520  irngnzply1  33681  qtophaus  33821  elzdif0  33965  measvunilem  34197  sibfof  34326  eulerpartlemb  34354  eulerpartlemf  34356  sseqf  34378  ballotlem5  34486  ballotlemi1  34489  ballotlemii  34490  ballotlemic  34493  ballotlem1c  34494  ballotlemscr  34505  ballotlemro  34509  ballotlemfg  34512  ballotlemfrc  34513  ballotlemfrceq  34515  ballotlemrinv0  34519  plymulx0  34533  signstfvn  34555  signsvfn  34568  bnj923  34753  bnj570  34890  bnj594  34897  subfacp1lem1  35161  satffunlem2lem1  35386  mrsubcn  35501  mrsubco  35503  circum  35656  dfon2lem6  35771  neibastop1  36342  bj-restn0b  37074  lindsadd  37602  lindsenlbs  37604  matunitlindflem1  37605  poimirlem24  37633  poimirlem25  37634  dvtan  37659  itg2addnclem2  37661  ftc1cnnc  37681  dvasin  37693  dvreasin  37695  dvreacos  37696  isdrngo2  37947  isdrngo3  37948  divrngidl  38017  isfldidl  38057  pridlc2  38061  pridlc3  38062  prter2  38869  lsateln0  38983  lsatlss  38984  lsmsat  38996  lsatcv0  39019  lsat0cv  39021  lcv1  39029  l1cvpat  39042  dih1dimatlem  41318  dihatexv2  41328  djhcvat42  41404  dihjat1lem  41417  dochsatshp  41440  lcfl6  41489  mapdrvallem2  41634  mapdpglem32  41694  idomnnzgmulnz  42116  aks6d1c5lem3  42120  aks6d1c5lem2  42121  deg1gprod  42123  sticksstones22  42151  unitscyglem4  42181  readvrec2  42344  readvrec  42345  readvcot  42347  evlsvvvallem  42544  evlsvvvallem2  42545  evlsvvval  42546  evlsbagval  42549  selvvvval  42568  evlselv  42570  evlsmhpvvval  42578  prjspertr  42588  prjsperref  42589  prjspersym  42590  prjspvs  42593  prjsprellsp  42594  dffltz  42617  irrapx1  42811  pell1234qrne0  42836  pell1234qrreccl  42837  pell1234qrmulcl  42838  pell14qrgt0  42842  pell1234qrdich  42844  pell14qrdich  42852  pell1qrge1  42853  pell1qr1  42854  pell1qrgap  42857  pell14qrgapw  42859  pellqrexplicit  42860  pellqrex  42862  pellfundge  42865  pellfundgt1  42866  setindtr  43008  kelac1  43047  mpaaeu  43134  flcidc  43154  deg1mhm  43184  onexoegt  43228  cantnfub  43305  cantnfresb  43308  succlg  43312  dflim5  43313  onmcl  43315  omabs2  43316  tfsconcatrev  43332  minregex2  43519  radcnvrat  44298  binomcxplemdvbinom  44337  disjiun2  45047  fiiuncl  45054  disjf1o  45180  difmapsn  45201  supminfxr2  45460  icoiccdif  45517  iccdificc  45532  fsumnncl  45565  fsumsupp0  45571  fprod0  45589  climrec  45596  islpcn  45632  lptre2pt  45633  limclner  45644  cnrefiisplem  45822  fprodcncf  45893  fperdvper  45912  dvdivcncf  45920  dvnmul  45936  dvmptfprodlem  45937  dvnprodlem2  45940  stoweidlem25  46018  stoweidlem28  46021  stoweidlem41  46034  stoweidlem44  46037  stoweidlem46  46039  stirlinglem5  46071  dirkercncflem1  46096  dirkercncflem2  46097  fourierdlem24  46124  fourierdlem62  46161  fouriersw  46224  fouriercn  46225  elaa2lem  46226  elaa2  46227  etransclem25  46252  etransclem35  46262  etransclem44  46271  sge0iunmptlemfi  46406  sge0fodjrnlem  46409  iundjiunlem  46452  meadjiunlem  46458  meaiininclem  46479  isomenndlem  46523  hsphoidmvle2  46578  hsphoidmvle  46579  hoidmv1lelem2  46585  hoidmvle  46593  ovnhoilem1  46594  hspdifhsp  46609  hspmbllem2  46620  ovnsubadd2lem  46638  ovolval4lem1  46642  preimagelt  46692  preimalegt  46693  fsummsndifre  47368  fsummmodsndifre  47370  odz2prm2pw  47559  fmtnoprmfac1lem  47560  fmtnoprmfac2lem1  47562  2pwp1prm  47585  lighneallem2  47602  lighneallem3  47603  lighneallem4  47606  bgoldbtbndlem2  47802  bgoldbtbndlem3  47803  bgoldbtbndlem4  47804  bgoldbtbnd  47805  isubgrvtxuhgr  47859  2zrngnmlid2  48240  mgpsumunsn  48344  mgpsumz  48345  mgpsumn  48346  lindslinindsimp1  48441  lindslinindsimp2  48447  lincresunit1  48461  lincresunit2  48462  lincresunit3lem1  48463  lincresunit3lem2  48464  lincresunit3  48465  lindssnlvec  48470  logcxp0  48519  relogbmulbexp  48545  relogbdivb  48546  dignn0fr  48585  rrxlinesc  48719  eenglngeehlnmlem1  48721  eenglngeehlnmlem2  48722