Theorem eldifi 4103

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939

This theorem is referenced by:  difss  4108  noelOLD  4297  eqoreldif  4622  xpdifid  6025  tz7.7  6217  tfi  7568  peano5  7605  wfrlem10  7964  wfrlem15  7969  tz7.48-1  8079  tz7.49  8081  dif20el  8130  oaf1o  8189  oeordi  8213  oeord  8214  oecan  8215  oeword  8216  oeworde  8219  oelimcl  8226  oeeulem  8227  oeeui  8228  oaabs2  8272  boxcutc  8505  domdifsn  8600  isinf  8731  pssnn  8736  pwfilem  8818  fsuppco2  8866  fsuppcor  8867  ordtypelem7  8988  unxpwdom2  9052  inf3lem3  9093  cantnfp1lem1  9141  cantnfp1lem3  9143  infxpenc2lem1  9445  dfacacn  9567  isf32lem3  9777  isf34lem4  9799  fin67  9817  isfin7-2  9818  domtriomlem  9864  axdc2lem  9870  axdc3lem4  9875  axdc4lem  9877  ttukeylem7  9937  konigthlem  9990  fpwwe2lem13  10064  fpwwe2  10065  modfzo0difsn  13312  hashf1lem1  13814  hashle2prv  13837  rlimrege0  14936  rlimrecl  14937  sumrblem  15068  fsumcvg  15069  summolem2a  15072  fsumss  15082  fsumless  15151  cvgcmpce  15173  binomlem  15184  incexclem  15191  incexc  15192  isumltss  15203  prodrblem  15283  fprodcvg  15284  prodmolem2a  15288  fprodss  15302  fprodn0f  15345  fprodeq0g  15348  fprodmodd  15351  rpnnen2lem10  15576  rpnnen2lem11  15577  sumeven  15738  sumodd  15739  lcmfunsnlem2  15984  oddprmge3  16044  oddprm  16147  nnoddn2prm  16148  nnoddn2prmb  16150  iserodd  16172  prmreclem2  16253  prmreclem3  16254  prmreclem5  16256  4sqlem19  16299  prmdvdsprmo  16378  prmodvdslcmf  16383  prmlem0  16439  firest  16706  grpinvnzcl  18171  symgextfv  18546  pmtrf  18583  pmtrdifellem3  18606  sylow2alem2  18743  sylow2a  18744  efgsf  18855  efgsrel  18860  efgs1  18861  efgsfo  18865  gsumzaddlem  19041  gsumzadd  19042  gsumzmhm  19057  gsum2d2lem  19093  dprdfadd  19142  dprdres  19150  subgdmdprd  19156  dmdprdsplitlem  19159  dmdprdsplit2lem  19167  dpjidcl  19180  ablfac1b  19192  pgpfac1lem1  19196  gsummgp0  19358  isirred  19449  irredrmul  19457  isdrng2  19512  isdrngd  19527  cntzsdrg  19581  lcomfsupp  19674  lbspropd  19871  lspsneq  19894  lsppratlem6  19924  lbsextlem2  19931  lbsextlem4  19933  ringelnzr  20039  psrbaglesupp  20148  psrlidm  20183  psrridm  20184  mplsubglem  20214  mpllsslem  20215  mplsubrglem  20219  mplmonmul  20245  mplcoe1  20246  mplcoe5  20249  mplbas2  20251  evlslem3  20293  mhpvscacl  20341  coe1tmmul2  20444  coe1tmmul  20445  xrs1mnd  20583  xrs10  20584  xrs1cmn  20585  cnsubrg  20605  psgnodpm  20732  zrhpsgnodpm  20736  evpmodpmf1o  20740  uvcresum  20937  frlmssuvc1  20938  frlmsslsp  20940  frlmup2  20943  lindfrn  20965  f1lindf  20966  lindfmm  20971  islindf4  20982  dmatmul  21106  1marepvsma1  21192  mdetdiaglem  21207  mdetrlin  21211  mdetrsca  21212  mdetralt  21217  maducoeval2  21249  madugsum  21252  symgmatr01  21263  gsummatr01lem3  21266  gsummatr01lem4  21267  gsummatr01  21268  smadiadetlem0  21270  smadiadetlem1a  21272  cmpfi  22016  2ndcdisj2  22065  elptr2  22182  ptcnplem  22229  xkopt  22263  kqdisj  22340  fin1aufil  22540  ptcmplem2  22661  ptcmplem3  22662  ptcmplem4  22663  opnsubg  22716  lpbl  23113  blcld  23115  zcld  23421  recld2  23422  reconnlem1  23434  divcn  23476  iundisj  24149  mbfeqalem1  24242  itg1val2  24285  itg1ge0  24287  i1fmullem  24295  i1fadd  24296  itg1addlem4  24300  itg1mulc  24305  itg1lea  24313  itg1le  24314  mbfi1fseqlem4  24319  itg2uba  24344  itg2lea  24345  itg2eqa  24346  itg2splitlem  24349  itg2split  24350  itgeqa  24414  ellimc3  24477  dvaddbr  24535  dvmulbr  24536  dvcobr  24543  dvcjbr  24546  dvrec  24552  dvrecg  24570  dvcnvlem  24573  dvexp3  24575  dveflem  24576  tdeglem4  24654  deg1n0ima  24683  deg1mul3le  24710  ig1peu  24765  ply1termlem  24793  plypf1  24802  plyaddlem1  24803  plymullem1  24804  coeeulem  24814  coeidlem  24827  coeid3  24830  coefv0  24838  coemulhi  24844  coemulc  24845  dvply1  24873  fta1  24897  vieta1lem2  24900  elaa  24905  elqaalem2  24909  aannenlem2  24918  aaliou2  24929  tayl0  24950  dvtaylp  24958  taylthlem1  24961  taylthlem2  24962  pserdvlem2  25016  logbcl  25345  relogbreexp  25353  relogbcxp  25363  cxplogb  25364  dcubic  25424  rlimcnp  25543  jensen  25566  dmgmaddn0  25600  dmlogdmgm  25601  lgamgulmlem2  25607  igamz  25625  gamp1  25635  regamcl  25638  wilthlem2  25646  basellem3  25660  chpub  25796  logexprlim  25801  lgslem1  25873  lgslem4  25876  lgsvalmod  25892  lgsqr  25927  lgsqrmod  25928  lgsqrmodndvds  25929  gausslemma2dlem0b  25933  gausslemma2dlem0c  25934  gausslemma2dlem0i  25940  gausslemma2dlem1a  25941  gausslemma2dlem4  25945  gausslemma2dlem5a  25946  gausslemma2dlem7  25949  gausslemma2d  25950  lgsquad2  25962  m1lgs  25964  2lgsoddprm  25992  2sqreultblem  26024  dchrisum0fno1  26087  rplogsum  26103  ishpg  26545  elntg2  26771  umgrislfupgrlem  26907  usgruspgrb  26966  nbumgrvtx  27128  nbupgrres  27146  isuvtx  27177  cusgrexilem2  27224  cusgrexi  27225  structtocusgr  27228  cusgrres  27230  cusgrfilem2  27238  vtxdginducedm1  27325  cusconngr  27970  2pthfrgr  28063  frgrncvvdeq  28088  frgrwopreglem4  28094  frgrwopreglem5  28100  frgrwopreg  28102  frgrhash2wsp  28111  strlem1  30027  strlem3  30030  strlem4  30031  strlem5  30032  hstrlem3  30038  hstrlem4  30039  iundisjf  30339  suppss3  30460  iundisjfi  30519  qtophaus  31100  elzdif0  31221  ind0  31277  measvunilem  31471  sibfof  31598  eulerpartlemb  31626  eulerpartlemf  31628  sseqf  31650  ballotlem5  31757  ballotlemi1  31760  ballotlemii  31761  ballotlemic  31764  ballotlem1c  31765  ballotlemscr  31776  ballotlemro  31780  ballotlemfg  31783  ballotlemfrc  31784  ballotlemfrceq  31786  ballotlemrinv0  31790  plymulx0  31817  signstfvn  31839  signsvfn  31852  bnj923  32039  bnj570  32177  bnj594  32184  subfacp1lem1  32426  satffunlem2lem1  32651  mrsubcn  32766  mrsubco  32768  circum  32917  dfon2lem6  33033  frrlem12  33134  frrlem13  33135  neibastop1  33707  bj-restn0b  34385  lindsadd  34900  lindsenlbs  34902  matunitlindflem1  34903  poimirlem24  34931  poimirlem25  34932  dvtan  34957  itg2addnclem2  34959  ftc1cnnc  34981  dvasin  34993  dvreasin  34995  dvreacos  34996  isdrngo2  35251  isdrngo3  35252  divrngidl  35321  isfldidl  35361  pridlc2  35365  pridlc3  35366  prter2  36032  lsateln0  36146  lsatlss  36147  lsmsat  36159  lsatcv0  36182  lsat0cv  36184  lcv1  36192  l1cvpat  36205  dih1dimatlem  38480  dihatexv2  38490  djhcvat42  38566  dihjat1lem  38579  dochsatshp  38602  lcfl6  38651  mapdrvallem2  38796  mapdpglem32  38856  prjspertr  39304  prjsperref  39305  prjspersym  39306  prjspvs  39309  prjsprellsp  39310  dffltz  39320  irrapx1  39474  pell1234qrne0  39499  pell1234qrreccl  39500  pell1234qrmulcl  39501  pell14qrgt0  39505  pell1234qrdich  39507  pell14qrdich  39515  pell1qrge1  39516  pell1qr1  39517  pell1qrgap  39520  pell14qrgapw  39522  pellqrexplicit  39523  pellqrex  39525  pellfundge  39528  pellfundgt1  39529  setindtr  39670  kelac1  39712  mpaaeu  39799  flcidc  39823  deg1mhm  39856  radcnvrat  40695  binomcxplemdvbinom  40734  disjiun2  41369  fiiuncl  41376  disjf1o  41501  difmapsn  41524  supminfxr2  41794  icoiccdif  41849  iccdificc  41864  fsumnncl  41901  fsumsplit1  41902  fsumsupp0  41908  fprod0  41926  climrec  41933  islpcn  41969  lptre2pt  41970  limclner  41981  cnrefiisplem  42159  fprodcncf  42233  fperdvper  42252  dvdivcncf  42261  dvnmul  42277  dvmptfprodlem  42278  dvnprodlem2  42281  stoweidlem25  42359  stoweidlem28  42362  stoweidlem41  42375  stoweidlem44  42378  stoweidlem46  42380  stirlinglem5  42412  dirkercncflem1  42437  dirkercncflem2  42438  fourierdlem24  42465  fourierdlem62  42502  fouriersw  42565  fouriercn  42566  elaa2lem  42567  elaa2  42568  etransclem25  42593  etransclem35  42603  etransclem44  42612  sge0iunmptlemfi  42744  sge0fodjrnlem  42747  iundjiunlem  42790  meadjiunlem  42796  meaiininclem  42817  isomenndlem  42861  hsphoidmvle2  42916  hsphoidmvle  42917  hoidmv1lelem2  42923  hoidmvle  42931  ovnhoilem1  42932  hspdifhsp  42947  hspmbllem2  42958  ovnsubadd2lem  42976  ovolval4lem1  42980  preimagelt  43029  preimalegt  43030  fsummsndifre  43581  fsummmodsndifre  43583  odz2prm2pw  43774  fmtnoprmfac1lem  43775  fmtnoprmfac2lem1  43777  2pwp1prm  43800  lighneallem2  43820  lighneallem3  43821  lighneallem4  43824  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  bgoldbtbndlem4  44022  bgoldbtbnd  44023  c0rhm  44232  c0rnghm  44233  zrrnghm  44237  2zrngnmlid2  44271  zrinitorngc  44320  zrtermorngc  44321  mgpsumunsn  44458  mgpsumz  44459  mgpsumn  44460  lindslinindsimp1  44561  lindslinindsimp2  44567  lincresunit1  44581  lincresunit2  44582  lincresunit3lem1  44583  lincresunit3lem2  44584  lincresunit3  44585  lindssnlvec  44590  logcxp0  44644  relogbmulbexp  44670  relogbdivb  44671  dignn0fr  44710  rrxlinesc  44771  eenglngeehlnmlem1  44773  eenglngeehlnmlem2  44774