Theorem eldifi 4094

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

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

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 3449  df-dif 3917

This theorem is referenced by:  difss  4099  eqoreldif  4649  xpdifid  6141  tz7.7  6358  tfi  7829  peano5  7869  resf1extb  7910  resf1ext2b  7911  xpord2pred  8124  frrlem12  8276  frrlem13  8277  tz7.48-1  8411  tz7.49  8413  dif20el  8469  oaf1o  8527  oeordi  8551  oeord  8552  oecan  8553  oeword  8554  oeworde  8557  oelimcl  8564  oeeulem  8565  oeeui  8566  oaabs2  8613  boxcutc  8914  domdifsn  9024  pssnn  9132  isinf  9207  isinfOLD  9208  pwfilem  9267  fsuppco2  9354  fsuppcor  9355  ordtypelem7  9477  unxpwdom2  9541  inf3lem3  9583  cantnfp1lem1  9631  cantnfp1lem3  9633  ttrcltr  9669  infxpenc2lem1  9972  dfacacn  10095  isf32lem3  10308  isf34lem4  10330  fin67  10348  isfin7-2  10349  domtriomlem  10395  axdc2lem  10401  axdc3lem4  10406  axdc4lem  10408  ttukeylem7  10468  konigthlem  10521  fpwwe2lem12  10595  fpwwe2  10596  modfzo0difsn  13908  hashf1lem1  14420  hashle2prv  14443  rlimrege0  15545  rlimrecl  15546  sumrblem  15677  fsumcvg  15678  summolem2a  15681  fsumss  15691  fsumsplit1  15711  fsumless  15762  cvgcmpce  15784  binomlem  15795  incexclem  15802  incexc  15803  isumltss  15814  prodrblem  15895  fprodcvg  15896  prodmolem2a  15900  fprodss  15914  fprodn0f  15957  fprodeq0g  15960  fprodmodd  15963  rpnnen2lem10  16191  rpnnen2lem11  16192  sumeven  16357  sumodd  16358  lcmfunsnlem2  16610  oddprmge3  16670  oddprm  16781  nnoddn2prm  16782  nnoddn2prmb  16784  iserodd  16806  prmreclem2  16888  prmreclem3  16889  prmreclem5  16891  4sqlem19  16934  prmdvdsprmo  17013  prmodvdslcmf  17018  prmlem0  17076  firest  17395  grpinvnzcl  18943  symgextfv  19348  pmtrf  19385  pmtrdifellem3  19408  sylow2alem2  19548  sylow2a  19549  efgsf  19659  efgsrel  19664  efgs1  19665  efgsfo  19669  gsumzaddlem  19851  gsumzadd  19852  gsumzmhm  19867  gsum2d2lem  19903  dprdfadd  19952  dprdres  19960  subgdmdprd  19966  dmdprdsplitlem  19969  dmdprdsplit2lem  19977  dpjidcl  19990  ablfac1b  20002  pgpfac1lem1  20006  gsummgp0  20227  isirred  20328  irredrmul  20336  ringelnzr  20432  c0rhm  20443  c0rnghm  20444  zrrnghm  20445  zrinitorngc  20551  zrtermorngc  20552  isdomn2  20620  isdomn4  20625  isdrng2  20652  drngmcl  20659  isdrngd  20674  isdrngdOLD  20676  imadrhmcl  20706  cntzsdrg  20711  lcomfsupp  20808  lbspropd  21006  lspsneq  21032  lsppratlem6  21062  lbsextlem2  21069  lbsextlem4  21071  xrs1mnd  21321  xrs10  21322  xrs1cmn  21323  cnsubrg  21344  psgnodpm  21497  zrhpsgnodpm  21501  evpmodpmf1o  21505  uvcresum  21702  frlmssuvc1  21703  frlmsslsp  21705  frlmup2  21708  lindfrn  21730  f1lindf  21731  lindfmm  21736  islindf4  21747  psrbaglesupp  21831  psrlidm  21871  psrridm  21872  mplsubglem  21908  mpllsslem  21909  mplsubrglem  21913  mplmonmul  21943  mplcoe1  21944  mplcoe5  21947  mplbas2  21949  evlslem3  21987  mhpvscacl  22041  psdmul  22053  coe1tmmul2  22162  coe1tmmul  22163  dmatmul  22384  1marepvsma1  22470  mdetdiaglem  22485  mdetrlin  22489  mdetrsca  22490  mdetralt  22495  maducoeval2  22527  madugsum  22530  symgmatr01  22541  gsummatr01lem3  22544  gsummatr01lem4  22545  gsummatr01  22546  smadiadetlem0  22548  smadiadetlem1a  22550  cmpfi  23295  2ndcdisj2  23344  elptr2  23461  ptcnplem  23508  xkopt  23542  kqdisj  23619  fin1aufil  23819  ptcmplem2  23940  ptcmplem3  23941  ptcmplem4  23942  opnsubg  23995  lpbl  24391  blcld  24393  zcld  24702  recld2  24703  reconnlem1  24715  divcnOLD  24757  divcn  24759  iundisj  25449  mbfeqalem1  25542  itg1val2  25585  itg1ge0  25587  i1fmullem  25595  i1fadd  25596  itg1addlem4  25600  itg1mulc  25605  itg1lea  25613  itg1le  25614  mbfi1fseqlem4  25619  itg2uba  25644  itg2lea  25645  itg2eqa  25646  itg2splitlem  25649  itg2split  25650  itgeqa  25715  ellimc3  25780  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcobr  25849  dvcobrOLD  25850  dvcjbr  25853  dvrec  25859  dvrecg  25877  dvcnvlem  25880  dvexp3  25882  dveflem  25883  tdeglem4  25965  deg1n0ima  25994  deg1mul3le  26022  ig1peu  26080  ply1termlem  26108  plypf1  26117  plyaddlem1  26118  plymullem1  26119  coeeulem  26129  coeidlem  26142  coeid3  26145  coefv0  26153  coemulhi  26159  coemulc  26160  dvply1  26191  fta1  26216  vieta1lem2  26219  elaa  26224  elqaalem2  26228  aannenlem2  26237  aaliou2  26248  tayl0  26269  dvtaylp  26278  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  pserdvlem2  26338  logbcl  26677  relogbreexp  26685  relogbcxp  26695  cxplogb  26696  dcubic  26756  rlimcnp  26875  jensen  26899  dmgmaddn0  26933  dmlogdmgm  26934  lgamgulmlem2  26940  igamz  26958  gamp1  26968  regamcl  26971  wilthlem2  26979  basellem3  26993  chpub  27131  logexprlim  27136  lgslem1  27208  lgslem4  27211  lgsvalmod  27227  lgsqr  27262  lgsqrmod  27263  lgsqrmodndvds  27264  gausslemma2dlem0b  27268  gausslemma2dlem0c  27269  gausslemma2dlem0i  27275  gausslemma2dlem1a  27276  gausslemma2dlem4  27280  gausslemma2dlem5a  27281  gausslemma2dlem7  27284  gausslemma2d  27285  lgsquad2  27297  m1lgs  27299  2lgsoddprm  27327  2sqreultblem  27359  dchrisum0fno1  27422  rplogsum  27438  ishpg  28686  elntg2  28912  umgrislfupgrlem  29049  usgruspgrb  29110  nbumgrvtx  29273  nbupgrres  29291  isuvtx  29322  cusgrexilem2  29369  cusgrexi  29370  structtocusgr  29373  cusgrres  29376  cusgrfilem2  29384  vtxdginducedm1  29471  cusconngr  30120  2pthfrgr  30213  frgrncvvdeq  30238  frgrwopreglem4  30244  frgrwopreglem5  30250  frgrwopreg  30252  frgrhash2wsp  30261  strlem1  32179  strlem3  32182  strlem4  32183  strlem5  32184  hstrlem3  32190  hstrlem4  32191  iundisjf  32518  suppss3  32647  iundisjfi  32719  suppssnn0  32730  ind0  32781  qsdrngi  33466  zringidom  33522  zringfrac  33525  irngnzply1  33686  qtophaus  33826  elzdif0  33970  measvunilem  34202  sibfof  34331  eulerpartlemb  34359  eulerpartlemf  34361  sseqf  34383  ballotlem5  34491  ballotlemi1  34494  ballotlemii  34495  ballotlemic  34498  ballotlem1c  34499  ballotlemscr  34510  ballotlemro  34514  ballotlemfg  34517  ballotlemfrc  34518  ballotlemfrceq  34520  ballotlemrinv0  34524  plymulx0  34538  signstfvn  34560  signsvfn  34573  bnj923  34758  bnj570  34895  bnj594  34902  subfacp1lem1  35166  satffunlem2lem1  35391  mrsubcn  35506  mrsubco  35508  circum  35661  dfon2lem6  35776  neibastop1  36347  bj-restn0b  37079  lindsadd  37607  lindsenlbs  37609  matunitlindflem1  37610  poimirlem24  37638  poimirlem25  37639  dvtan  37664  itg2addnclem2  37666  ftc1cnnc  37686  dvasin  37698  dvreasin  37700  dvreacos  37701  isdrngo2  37952  isdrngo3  37953  divrngidl  38022  isfldidl  38062  pridlc2  38066  pridlc3  38067  prter2  38874  lsateln0  38988  lsatlss  38989  lsmsat  39001  lsatcv0  39024  lsat0cv  39026  lcv1  39034  l1cvpat  39047  dih1dimatlem  41323  dihatexv2  41333  djhcvat42  41409  dihjat1lem  41422  dochsatshp  41445  lcfl6  41494  mapdrvallem2  41639  mapdpglem32  41699  idomnnzgmulnz  42121  aks6d1c5lem3  42125  aks6d1c5lem2  42126  deg1gprod  42128  sticksstones22  42156  unitscyglem4  42186  readvrec2  42349  readvrec  42350  readvcot  42352  evlsvvvallem  42549  evlsvvvallem2  42550  evlsvvval  42551  evlsbagval  42554  selvvvval  42573  evlselv  42575  evlsmhpvvval  42583  prjspertr  42593  prjsperref  42594  prjspersym  42595  prjspvs  42598  prjsprellsp  42599  dffltz  42622  irrapx1  42816  pell1234qrne0  42841  pell1234qrreccl  42842  pell1234qrmulcl  42843  pell14qrgt0  42847  pell1234qrdich  42849  pell14qrdich  42857  pell1qrge1  42858  pell1qr1  42859  pell1qrgap  42862  pell14qrgapw  42864  pellqrexplicit  42865  pellqrex  42867  pellfundge  42870  pellfundgt1  42871  setindtr  43013  kelac1  43052  mpaaeu  43139  flcidc  43159  deg1mhm  43189  onexoegt  43233  cantnfub  43310  cantnfresb  43313  succlg  43317  dflim5  43318  onmcl  43320  omabs2  43321  tfsconcatrev  43337  minregex2  43524  radcnvrat  44303  binomcxplemdvbinom  44342  disjiun2  45052  fiiuncl  45059  disjf1o  45185  difmapsn  45206  supminfxr2  45465  icoiccdif  45522  iccdificc  45537  fsumnncl  45570  fsumsupp0  45576  fprod0  45594  climrec  45601  islpcn  45637  lptre2pt  45638  limclner  45649  cnrefiisplem  45827  fprodcncf  45898  fperdvper  45917  dvdivcncf  45925  dvnmul  45941  dvmptfprodlem  45942  dvnprodlem2  45945  stoweidlem25  46023  stoweidlem28  46026  stoweidlem41  46039  stoweidlem44  46042  stoweidlem46  46044  stirlinglem5  46076  dirkercncflem1  46101  dirkercncflem2  46102  fourierdlem24  46129  fourierdlem62  46166  fouriersw  46229  fouriercn  46230  elaa2lem  46231  elaa2  46232  etransclem25  46257  etransclem35  46267  etransclem44  46276  sge0iunmptlemfi  46411  sge0fodjrnlem  46414  iundjiunlem  46457  meadjiunlem  46463  meaiininclem  46484  isomenndlem  46528  hsphoidmvle2  46583  hsphoidmvle  46584  hoidmv1lelem2  46590  hoidmvle  46598  ovnhoilem1  46599  hspdifhsp  46614  hspmbllem2  46625  ovnsubadd2lem  46643  ovolval4lem1  46647  preimagelt  46697  preimalegt  46698  fsummsndifre  47373  fsummmodsndifre  47375  odz2prm2pw  47564  fmtnoprmfac1lem  47565  fmtnoprmfac2lem1  47567  2pwp1prm  47590  lighneallem2  47607  lighneallem3  47608  lighneallem4  47611  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbndlem4  47809  bgoldbtbnd  47810  isubgrvtxuhgr  47864  2zrngnmlid2  48245  mgpsumunsn  48349  mgpsumz  48350  mgpsumn  48351  lindslinindsimp1  48446  lindslinindsimp2  48452  lincresunit1  48466  lincresunit2  48467  lincresunit3lem1  48468  lincresunit3lem2  48469  lincresunit3  48470  lindssnlvec  48475  logcxp0  48524  relogbmulbexp  48550  relogbdivb  48551  dignn0fr  48590  rrxlinesc  48724  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727