Theorem eldifi 4113

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2107   ∖ cdif 3930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3466  df-dif 3936

This theorem is referenced by:  difss  4118  eqoreldif  4667  xpdifid  6170  tz7.7  6391  tfi  7857  peano5  7898  resf1extb  7939  resf1ext2b  7940  xpord2pred  8153  frrlem12  8305  frrlem13  8306  wfrlem10OLD  8341  wfrlem15OLD  8346  tz7.48-1  8466  tz7.49  8468  dif20el  8526  oaf1o  8584  oeordi  8608  oeord  8609  oecan  8610  oeword  8611  oeworde  8614  oelimcl  8621  oeeulem  8622  oeeui  8623  oaabs2  8670  boxcutc  8964  domdifsn  9077  pssnn  9191  isinf  9279  isinfOLD  9280  pwfilem  9339  fsuppco2  9426  fsuppcor  9427  ordtypelem7  9547  unxpwdom2  9611  inf3lem3  9653  cantnfp1lem1  9701  cantnfp1lem3  9703  ttrcltr  9739  infxpenc2lem1  10042  dfacacn  10165  isf32lem3  10378  isf34lem4  10400  fin67  10418  isfin7-2  10419  domtriomlem  10465  axdc2lem  10471  axdc3lem4  10476  axdc4lem  10478  ttukeylem7  10538  konigthlem  10591  fpwwe2lem12  10665  fpwwe2  10666  modfzo0difsn  13967  hashf1lem1  14477  hashle2prv  14500  rlimrege0  15598  rlimrecl  15599  sumrblem  15730  fsumcvg  15731  summolem2a  15734  fsumss  15744  fsumsplit1  15764  fsumless  15815  cvgcmpce  15837  binomlem  15848  incexclem  15855  incexc  15856  isumltss  15867  prodrblem  15948  fprodcvg  15949  prodmolem2a  15953  fprodss  15967  fprodn0f  16010  fprodeq0g  16013  fprodmodd  16016  rpnnen2lem10  16242  rpnnen2lem11  16243  sumeven  16407  sumodd  16408  lcmfunsnlem2  16660  oddprmge3  16720  oddprm  16831  nnoddn2prm  16832  nnoddn2prmb  16834  iserodd  16856  prmreclem2  16938  prmreclem3  16939  prmreclem5  16941  4sqlem19  16984  prmdvdsprmo  17063  prmodvdslcmf  17068  prmlem0  17126  firest  17453  grpinvnzcl  19003  symgextfv  19409  pmtrf  19446  pmtrdifellem3  19469  sylow2alem2  19609  sylow2a  19610  efgsf  19720  efgsrel  19725  efgs1  19726  efgsfo  19730  gsumzaddlem  19912  gsumzadd  19913  gsumzmhm  19928  gsum2d2lem  19964  dprdfadd  20013  dprdres  20021  subgdmdprd  20027  dmdprdsplitlem  20030  dmdprdsplit2lem  20038  dpjidcl  20051  ablfac1b  20063  pgpfac1lem1  20067  gsummgp0  20288  isirred  20392  irredrmul  20400  ringelnzr  20496  c0rhm  20507  c0rnghm  20508  zrrnghm  20509  zrinitorngc  20615  zrtermorngc  20616  isdomn2  20684  isdomn4  20689  isdrng2  20716  drngmcl  20723  isdrngd  20738  isdrngdOLD  20740  imadrhmcl  20771  cntzsdrg  20776  lcomfsupp  20873  lbspropd  21071  lspsneq  21097  lsppratlem6  21127  lbsextlem2  21134  lbsextlem4  21136  xrs1mnd  21389  xrs10  21390  xrs1cmn  21391  cnsubrg  21412  psgnodpm  21573  zrhpsgnodpm  21577  evpmodpmf1o  21581  uvcresum  21780  frlmssuvc1  21781  frlmsslsp  21783  frlmup2  21786  lindfrn  21808  f1lindf  21809  lindfmm  21814  islindf4  21825  psrbaglesupp  21909  psrlidm  21949  psrridm  21950  mplsubglem  21986  mpllsslem  21987  mplsubrglem  21991  mplmonmul  22021  mplcoe1  22022  mplcoe5  22025  mplbas2  22027  evlslem3  22071  mhpvscacl  22125  psdmul  22137  coe1tmmul2  22246  coe1tmmul  22247  dmatmul  22470  1marepvsma1  22556  mdetdiaglem  22571  mdetrlin  22575  mdetrsca  22576  mdetralt  22581  maducoeval2  22613  madugsum  22616  symgmatr01  22627  gsummatr01lem3  22630  gsummatr01lem4  22631  gsummatr01  22632  smadiadetlem0  22634  smadiadetlem1a  22636  cmpfi  23381  2ndcdisj2  23430  elptr2  23547  ptcnplem  23594  xkopt  23628  kqdisj  23705  fin1aufil  23905  ptcmplem2  24026  ptcmplem3  24027  ptcmplem4  24028  opnsubg  24081  lpbl  24479  blcld  24481  zcld  24790  recld2  24791  reconnlem1  24803  divcnOLD  24845  divcn  24847  iundisj  25538  mbfeqalem1  25631  itg1val2  25674  itg1ge0  25676  i1fmullem  25684  i1fadd  25685  itg1addlem4  25689  itg1mulc  25694  itg1lea  25702  itg1le  25703  mbfi1fseqlem4  25708  itg2uba  25733  itg2lea  25734  itg2eqa  25735  itg2splitlem  25738  itg2split  25739  itgeqa  25804  ellimc3  25869  dvaddbr  25929  dvmulbr  25930  dvmulbrOLD  25931  dvcobr  25938  dvcobrOLD  25939  dvcjbr  25942  dvrec  25948  dvrecg  25966  dvcnvlem  25969  dvexp3  25971  dveflem  25972  tdeglem4  26054  deg1n0ima  26083  deg1mul3le  26111  ig1peu  26169  ply1termlem  26197  plypf1  26206  plyaddlem1  26207  plymullem1  26208  coeeulem  26218  coeidlem  26231  coeid3  26234  coefv0  26242  coemulhi  26248  coemulc  26249  dvply1  26280  fta1  26305  vieta1lem2  26308  elaa  26313  elqaalem2  26317  aannenlem2  26326  aaliou2  26337  tayl0  26358  dvtaylp  26367  taylthlem1  26370  taylthlem2  26371  taylthlem2OLD  26372  pserdvlem2  26427  logbcl  26765  relogbreexp  26773  relogbcxp  26783  cxplogb  26784  dcubic  26844  rlimcnp  26963  jensen  26987  dmgmaddn0  27021  dmlogdmgm  27022  lgamgulmlem2  27028  igamz  27046  gamp1  27056  regamcl  27059  wilthlem2  27067  basellem3  27081  chpub  27219  logexprlim  27224  lgslem1  27296  lgslem4  27299  lgsvalmod  27315  lgsqr  27350  lgsqrmod  27351  lgsqrmodndvds  27352  gausslemma2dlem0b  27356  gausslemma2dlem0c  27357  gausslemma2dlem0i  27363  gausslemma2dlem1a  27364  gausslemma2dlem4  27368  gausslemma2dlem5a  27369  gausslemma2dlem7  27372  gausslemma2d  27373  lgsquad2  27385  m1lgs  27387  2lgsoddprm  27415  2sqreultblem  27447  dchrisum0fno1  27510  rplogsum  27526  ishpg  28722  elntg2  28949  umgrislfupgrlem  29086  usgruspgrb  29147  nbumgrvtx  29310  nbupgrres  29328  isuvtx  29359  cusgrexilem2  29406  cusgrexi  29407  structtocusgr  29410  cusgrres  29413  cusgrfilem2  29421  vtxdginducedm1  29508  cusconngr  30157  2pthfrgr  30250  frgrncvvdeq  30275  frgrwopreglem4  30281  frgrwopreglem5  30287  frgrwopreg  30289  frgrhash2wsp  30298  strlem1  32216  strlem3  32219  strlem4  32220  strlem5  32221  hstrlem3  32227  hstrlem4  32228  iundisjf  32549  suppss3  32682  iundisjfi  32745  suppssnn0  32756  ind0  32790  qsdrngi  33464  zringidom  33520  zringfrac  33523  irngnzply1  33682  qtophaus  33776  elzdif0  33922  measvunilem  34154  sibfof  34283  eulerpartlemb  34311  eulerpartlemf  34313  sseqf  34335  ballotlem5  34443  ballotlemi1  34446  ballotlemii  34447  ballotlemic  34450  ballotlem1c  34451  ballotlemscr  34462  ballotlemro  34466  ballotlemfg  34469  ballotlemfrc  34470  ballotlemfrceq  34472  ballotlemrinv0  34476  plymulx0  34503  signstfvn  34525  signsvfn  34538  bnj923  34723  bnj570  34860  bnj594  34867  subfacp1lem1  35125  satffunlem2lem1  35350  mrsubcn  35465  mrsubco  35467  circum  35620  dfon2lem6  35730  neibastop1  36301  bj-restn0b  37033  lindsadd  37561  lindsenlbs  37563  matunitlindflem1  37564  poimirlem24  37592  poimirlem25  37593  dvtan  37618  itg2addnclem2  37620  ftc1cnnc  37640  dvasin  37652  dvreasin  37654  dvreacos  37655  isdrngo2  37906  isdrngo3  37907  divrngidl  37976  isfldidl  38016  pridlc2  38020  pridlc3  38021  prter2  38823  lsateln0  38937  lsatlss  38938  lsmsat  38950  lsatcv0  38973  lsat0cv  38975  lcv1  38983  l1cvpat  38996  dih1dimatlem  41272  dihatexv2  41282  djhcvat42  41358  dihjat1lem  41371  dochsatshp  41394  lcfl6  41443  mapdrvallem2  41588  mapdpglem32  41648  idomnnzgmulnz  42075  aks6d1c5lem3  42079  aks6d1c5lem2  42080  deg1gprod  42082  sticksstones22  42110  unitscyglem4  42140  readvrec2  42336  readvrec  42337  readvcot  42339  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  43127  deg1mhm  43157  onexoegt  43201  cantnfub  43279  cantnfresb  43282  succlg  43286  dflim5  43287  onmcl  43289  omabs2  43290  tfsconcatrev  43306  minregex2  43493  radcnvrat  44278  binomcxplemdvbinom  44317  disjiun2  45008  fiiuncl  45015  disjf1o  45141  difmapsn  45162  supminfxr2  45425  icoiccdif  45482  iccdificc  45497  fsumnncl  45532  fsumsupp0  45538  fprod0  45556  climrec  45563  islpcn  45599  lptre2pt  45600  limclner  45611  cnrefiisplem  45789  fprodcncf  45860  fperdvper  45879  dvdivcncf  45887  dvnmul  45903  dvmptfprodlem  45904  dvnprodlem2  45907  stoweidlem25  45985  stoweidlem28  45988  stoweidlem41  46001  stoweidlem44  46004  stoweidlem46  46006  stirlinglem5  46038  dirkercncflem1  46063  dirkercncflem2  46064  fourierdlem24  46091  fourierdlem62  46128  fouriersw  46191  fouriercn  46192  elaa2lem  46193  elaa2  46194  etransclem25  46219  etransclem35  46229  etransclem44  46238  sge0iunmptlemfi  46373  sge0fodjrnlem  46376  iundjiunlem  46419  meadjiunlem  46425  meaiininclem  46446  isomenndlem  46490  hsphoidmvle2  46545  hsphoidmvle  46546  hoidmv1lelem2  46552  hoidmvle  46560  ovnhoilem1  46561  hspdifhsp  46576  hspmbllem2  46587  ovnsubadd2lem  46605  ovolval4lem1  46609  preimagelt  46659  preimalegt  46660  fsummsndifre  47305  fsummmodsndifre  47307  odz2prm2pw  47496  fmtnoprmfac1lem  47497  fmtnoprmfac2lem1  47499  2pwp1prm  47522  lighneallem2  47539  lighneallem3  47540  lighneallem4  47543  bgoldbtbndlem2  47739  bgoldbtbndlem3  47740  bgoldbtbndlem4  47741  bgoldbtbnd  47742  isubgrvtxuhgr  47796  2zrngnmlid2  48119  mgpsumunsn  48223  mgpsumz  48224  mgpsumn  48225  lindslinindsimp1  48320  lindslinindsimp2  48326  lincresunit1  48340  lincresunit2  48341  lincresunit3lem1  48342  lincresunit3lem2  48343  lincresunit3  48344  lindssnlvec  48349  logcxp0  48402  relogbmulbexp  48428  relogbdivb  48429  dignn0fr  48468  rrxlinesc  48602  eenglngeehlnmlem1  48604  eenglngeehlnmlem2  48605