Theorem eldifi 4067

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2144   ∖ cdif 4045

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 4047

This theorem is used by:  difss  4072  eqoreldif  4645  xpdifid  6158  xpdifcnvepel  6159  tz7.7  6388  tfi  7864  peano5  7905  resf1extb  7946  resf1ext2b  7947  xpord2pred  8162  frrlem12  8315  frrlem13  8316  tz7.48-1  8453  tz7.49  8455  dif20el  8513  oaf1o  8571  oeordi  8596  oeord  8597  oecan  8598  oeword  8599  oeworde  8602  oelimcl  8609  oeeulem  8610  oeeui  8611  oaabs2  8658  boxcutc  8969  domdifsn  9079  pssnn  9184  isinf  9256  pwfilem  9309  fsuppco2  9395  fsuppcor  9396  ordtypelem7  9518  unxpwdom2  9582  inf3lem3  9631  cantnfp1lem1  9679  cantnfp1lem3  9681  ttrcltr  9717  elhf3OLD  9923  infxpenc2lem1  10098  dfacacn  10220  isf32lem3  10433  isf34lem4  10455  fin67  10473  isfin7-2  10474  domtriomlem  10520  axdc2lem  10526  axdc3lem4  10531  axdc4lem  10533  ttukeylem7  10593  konigthlem  10653  fpwwe2lem12  10727  fpwwe2  10728  ind0  12330  modfzo0difsn  14086  hashf1lem1  14600  hashle2prv  14623  rlimrege0  15746  rlimrecl  15747  sumrblem  15877  fsumcvg  15878  summolem2a  15881  fsumss  15891  fsumsplit1  15911  fsumless  15963  cvgcmpce  15985  binomlem  15998  incexclem  16005  incexc  16006  isumltss  16017  prodrblem  16096  fprodcvg  16097  prodmolem2a  16101  fprodss  16115  fprodn0f  16158  fprodeq0g  16161  fprodmodd  16164  rpnnen2lem10  16391  rpnnen2lem11  16392  sumeven  16557  sumodd  16558  lcmfunsnlem2  16815  oddprmge3  16876  oddprm  16988  nnoddn2prm  16989  nnoddn2prmb  16991  iserodd  17013  prmreclem2  17095  prmreclem3  17096  prmreclem5  17098  4sqlem19  17141  prmdvdsprmo  17220  prmodvdslcmf  17225  prmlem0  17283  firest  17603  chnccat  18800  chnrev  18801  grpinvnzcl  19221  symgextfv  19632  pmtrf  19669  pmtrdifellem3  19692  sylow2alem2  19832  sylow2a  19833  efgsf  19943  efgsrel  19948  efgs1  19949  efgsfo  19953  gsumzaddlem  20135  gsumzadd  20136  gsumzmhm  20151  gsum2d2lem  20187  dprdfadd  20236  dprdres  20244  subgdmdprd  20250  dmdprdsplitlem  20253  dmdprdsplit2lem  20261  dpjidcl  20274  ablfac1b  20286  pgpfac1lem1  20290  gsummgp0  20547  isirred  20649  irredrmul  20657  ringelnzr  20774  c0rhm  20786  c0rnghm  20787  zrrnghm  20788  zrinitorngc  20894  zrtermorngc  20895  isdomn2  20963  isdomn4  20967  isdrng2  20997  isdrng3lem2  21006  isdrng5  21008  drngmcl  21009  isdrngd  21022  isdrngdOLD  21024  imadrhmcl  21054  cntzsdrg  21059  lcomfsupp  21177  lbspropd  21374  lspsneq  21400  lsppratlem6  21430  lbsextlem2  21437  lbsextlem4  21439  prmidlc2  21630  cmprmidlmcl  21631  cnsubrg  21733  xrs1mnd  21746  xrs10  21747  xrs1cmn  21748  psgnodpm  21894  zrhpsgnodpm  21898  evpmodpmf1o  21902  uvcresum  22099  frlmssuvc1  22100  frlmsslsp  22102  frlmup2  22105  lindfrn  22127  f1lindf  22128  lindfmm  22133  islindf4  22144  lindsenlbs  22157  psrbaglesupp  22230  psrlidm  22269  psrridm  22270  mplsubglem  22306  mpllsslem  22307  mplsubrglem  22311  mplmonmul  22345  mplcoe1  22346  mplcoe5  22349  mplbas2  22351  evlslem3  22389  evlsvvvallem  22400  evlsvvvallem2  22401  evlsvvval  22402  selvvvval  22451  mhpvscacl  22475  psdmul  22487  coe1tmmul2  22595  coe1tmmul  22596  dmatmul  22812  1marepvsma1  22898  mdetdiaglem  22913  mdetrlin  22917  mdetrsca  22918  mdetralt  22923  maducoeval2  22955  madugsum  22958  symgmatr01  22969  gsummatr01lem3  22972  gsummatr01lem4  22973  gsummatr01  22974  smadiadetlem0  22976  smadiadetlem1a  22978  matunitlindflem1  22994  cmpfi  23726  2ndcdisj2  23776  elptr2  23893  ptcnplem  23940  xkopt  23974  kqdisj  24051  fin1aufil  24251  ptcmplem2  24372  ptcmplem3  24373  ptcmplem4  24374  opnsubg  24427  lpbl  24822  blcld  24824  zcld  25133  recld2  25134  reconnlem1  25146  divcn  25189  iundisj  25869  mbfeqalem1  25962  itg1val2  26005  itg1ge0  26007  i1fmullem  26015  i1fadd  26016  itg1addlem4  26020  itg1mulc  26025  itg1lea  26033  itg1le  26034  mbfi1fseqlem4  26039  itg2uba  26064  itg2lea  26065  itg2eqa  26066  itg2splitlem  26069  itg2split  26070  itgeqa  26134  ellimc3  26199  dvaddbr  26258  dvmulbr  26259  dvcobr  26266  dvcjbr  26269  dvrec  26275  dvrecg  26293  dvcnvlem  26296  dvexp3  26298  dveflem  26299  tdeglem4  26378  deg1n0ima  26407  deg1mul3le  26435  ig1peu  26493  ply1termlem  26521  plypf1  26531  plyaddlem1  26532  plymullem1  26533  coeeulem  26543  coeidlem  26556  coeid3  26559  coefv0  26567  coemulhi  26573  coemulc  26574  plyn0mulidp  26602  dvply1  26605  fta1  26629  vieta1lem2  26634  elaa  26639  elqaalem2  26643  preimaaa  26646  aannenlem2  26656  aaliou2  26667  tayl0  26689  dvtaylp  26697  taylthlem1  26700  taylthlem2  26701  pserdvlem2  26755  logbcl  27095  relogbreexp  27103  relogbcxp  27113  cxplogb  27114  dcubic  27174  rlimcnp  27293  jensen  27316  dmgmaddn0  27350  dmlogdmgm  27351  lgamgulmlem2  27357  igamz  27375  gamp1  27385  regamcl  27388  wilthlem2  27396  basellem3  27410  chpub  27547  logexprlim  27552  lgslem1  27624  lgslem4  27627  lgsvalmod  27643  lgsqr  27678  lgsqrmod  27679  lgsqrmodndvds  27680  gausslemma2dlem0b  27684  gausslemma2dlem0c  27685  gausslemma2dlem0i  27691  gausslemma2dlem1a  27692  gausslemma2dlem4  27696  gausslemma2dlem5a  27697  gausslemma2dlem7  27700  gausslemma2d  27701  lgsquad2  27713  m1lgs  27715  2lgsoddprm  27743  2sqreultblem  27775  dchrisum0fno1  27838  rplogsum  27854  ishpg  29237  elntg2  29563  umgrislfupgrlem  29700  usgruspgrb  29764  nbumgrvtx  29927  nbupgrres  29945  isuvtx  29976  cusgrexilem2  30023  cusgrexi  30024  structtocusgr  30027  cusgrres  30029  cusgrfilem2  30037  vtxdginducedm1  30124  cusconngr  30792  2pthfrgr  30885  frgrncvvdeq  30910  frgrwopreglem4  30916  frgrwopreglem5  30922  frgrwopreg  30924  frgrhash2wsp  30933  strlem1  32852  strlem3  32855  strlem4  32856  strlem5  32857  hstrlem3  32863  hstrlem4  32864  iundisjf  33183  suppss3  33315  iundisjfi  33388  suppssnn0  33397  qsdrngi  34019  zringidom  34083  zringfrac  34086  psrmonmul  34182  irngnzply1  34323  qtophaus  34468  elzdif0  34612  measvunilem  34845  sibfof  34972  eulerpartlemb  35000  eulerpartlemf  35002  sseqf  35024  ballotlem5  35132  ballotlemi1  35135  ballotlemii  35136  ballotlemic  35139  ballotlem1c  35140  ballotlemscr  35151  ballotlemro  35155  ballotlemfg  35158  ballotlemfrc  35159  ballotlemfrceq  35161  ballotlemrinv0  35165  signstfvn  35198  signsvfn  35211  bnj923  35399  bnj570  35535  bnj594  35542  acwer1prc  35760  fineqvnttrclselem1  35789  fineqvnttrclselem2  35790  fineqvnttrclselem3  35791  fineqvnttrclse  35792  subfacp1lem1  35944  satffunlem2lem1  36169  mrsubcn  36284  mrsubco  36286  circum  36439  dfon2lem6  36550  neibastop1  37147  bj-restn0b  38012  lindsadd  38537  poimirlem24  38563  poimirlem25  38564  dvtan  38589  itg2addnclem2  38591  ftc1cnnc  38611  dvasin  38623  dvreasin  38625  dvreacos  38626  isdrngo2  38893  isdrngo3  38894  divrngidl  38963  isfldidl  39003  pridlc2  39007  pridlc3  39008  blockadjliftmap  39391  prter2  39939  lsateln0  40053  lsatlss  40054  lsmsat  40066  lsatcv0  40089  lsat0cv  40091  lcv1  40099  l1cvpat  40112  dih1dimatlem  42387  dihatexv2  42397  djhcvat42  42473  dihjat1lem  42486  dochsatshp  42509  lcfl6  42558  mapdrvallem2  42703  mapdpglem32  42763  idomnnzgmulnz  43184  aks6d1c5lem3  43188  aks6d1c5lem2  43189  deg1gprod  43191  sticksstones22  43219  unitscyglem4  43249  readvrec2  43413  readvrec  43414  readvcot  43416  evlsbagval  43615  evlselv  43618  evlsmhpvvval  43624  prjspertr  43634  prjsperref  43635  prjspersym  43636  prjspvs  43639  prjsprellsp  43640  dffltz  43671  irrapx1  43835  pell1234qrne0  43860  pell1234qrreccl  43861  pell1234qrmulcl  43862  pell14qrgt0  43866  pell1234qrdich  43868  pell14qrdich  43876  pell1qrge1  43877  pell1qr1  43878  pell1qrgap  43881  pell14qrgapw  43883  pellqrexplicit  43884  pellqrex  43886  pellfundge  43889  pellfundgt1  43890  setindtr  44031  kelac1  44065  mpaaeu  44152  flcidc  44172  deg1mhm  44202  onexoegt  44246  cantnfub  44323  cantnfresb  44326  succlg  44330  dflim5  44331  onmcl  44333  omabs2  44334  tfsconcatrev  44350  minregex2  44536  radcnvrat  45298  binomcxplemdvbinom  45337  disjiun2  46075  fiiuncl  46082  disjf1o  46206  difmapsn  46225  supminfxr2  46479  icoiccdif  46536  iccdificc  46551  fsumnncl  46584  fsumsupp0  46590  fprod0  46608  climrec  46615  islpcn  46649  lptre2pt  46650  limclner  46661  cnrefiisplem  46839  fprodcncf  46910  fperdvper  46929  dvdivcncf  46937  dvnmul  46953  dvmptfprodlem  46954  dvnprodlem2  46957  stoweidlem25  47035  stoweidlem28  47038  stoweidlem41  47051  stoweidlem44  47054  stoweidlem46  47056  stirlinglem5  47088  dirkercncflem1  47113  dirkercncflem2  47114  fourierdlem24  47141  fourierdlem62  47178  fouriersw  47241  fouriercn  47242  elaa2lem  47243  elaa2  47244  etransclem25  47269  etransclem35  47279  etransclem44  47288  sge0iunmptlemfi  47423  sge0fodjrnlem  47426  iundjiunlem  47469  meadjiunlem  47475  meaiininclem  47496  isomenndlem  47540  hsphoidmvle2  47595  hsphoidmvle  47596  hoidmv1lelem2  47602  hoidmvle  47610  ovnhoilem1  47611  hspdifhsp  47626  hspmbllem2  47637  ovnsubadd2lem  47655  ovolval4lem1  47659  preimagelt  47709  preimalegt  47710  chnsubseq  47890  tmachlem-tpopen  47951  fsummsndifre  48450  fsummmodsndifre  48452  odz2prm2pw  48648  fmtnoprmfac1lem  48649  fmtnoprmfac2lem1  48651  2pwp1prm  48674  lighneallem2  48691  lighneallem3  48692  lighneallem4  48695  bgoldbtbndlem2  48904  bgoldbtbndlem3  48905  bgoldbtbndlem4  48906  bgoldbtbnd  48907  isubgrvtxuhgr  48962  2zrngnmlid2  49354  mgpsumunsn  49473  mgpsumz  49474  mgpsumn  49475  lindslinindsimp1  49569  lindslinindsimp2  49575  lincresunit1  49589  lincresunit2  49590  lincresunit3lem1  49591  lincresunit3lem2  49592  lincresunit3  49593  lindssnlvec  49598  logcxp0  49647  relogbmulbexp  49673  relogbdivb  49674  dignn0fr  49713  rrxlinesc  49847  eenglngeehlnmlem1  49849  eenglngeehlnmlem2  49850