Theorem eldifi 4062

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-dif 3891

This theorem is referenced by:  difss  4067  eqoreldif  4621  xpdifid  6076  tz7.7  6296  tfi  7709  peano5  7749  peano5OLD  7750  frrlem12  8122  frrlem13  8123  wfrlem10OLD  8158  wfrlem15OLD  8163  tz7.48-1  8283  tz7.49  8285  dif20el  8344  oaf1o  8403  oeordi  8427  oeord  8428  oecan  8429  oeword  8430  oeworde  8433  oelimcl  8440  oeeulem  8441  oeeui  8442  oaabs2  8488  boxcutc  8738  domdifsn  8850  pssnn  8960  pwfilem  8969  isinf  9045  pssnnOLD  9049  pwfilemOLD  9122  fsuppco2  9171  fsuppcor  9172  ordtypelem7  9292  unxpwdom2  9356  inf3lem3  9397  cantnfp1lem1  9445  cantnfp1lem3  9447  ttrcltr  9483  infxpenc2lem1  9784  dfacacn  9906  isf32lem3  10120  isf34lem4  10142  fin67  10160  isfin7-2  10161  domtriomlem  10207  axdc2lem  10213  axdc3lem4  10218  axdc4lem  10220  ttukeylem7  10280  konigthlem  10333  fpwwe2lem12  10407  fpwwe2  10408  modfzo0difsn  13672  hashf1lem1  14177  hashf1lem1OLD  14178  hashle2prv  14201  rlimrege0  15297  rlimrecl  15298  sumrblem  15432  fsumcvg  15433  summolem2a  15436  fsumss  15446  fsumsplit1  15466  fsumless  15517  cvgcmpce  15539  binomlem  15550  incexclem  15557  incexc  15558  isumltss  15569  prodrblem  15648  fprodcvg  15649  prodmolem2a  15653  fprodss  15667  fprodn0f  15710  fprodeq0g  15713  fprodmodd  15716  rpnnen2lem10  15941  rpnnen2lem11  15942  sumeven  16105  sumodd  16106  lcmfunsnlem2  16354  oddprmge3  16414  oddprm  16520  nnoddn2prm  16521  nnoddn2prmb  16523  iserodd  16545  prmreclem2  16627  prmreclem3  16628  prmreclem5  16630  4sqlem19  16673  prmdvdsprmo  16752  prmodvdslcmf  16757  prmlem0  16816  firest  17152  grpinvnzcl  18656  symgextfv  19035  pmtrf  19072  pmtrdifellem3  19095  sylow2alem2  19232  sylow2a  19233  efgsf  19344  efgsrel  19349  efgs1  19350  efgsfo  19354  gsumzaddlem  19531  gsumzadd  19532  gsumzmhm  19547  gsum2d2lem  19583  dprdfadd  19632  dprdres  19640  subgdmdprd  19646  dmdprdsplitlem  19649  dmdprdsplit2lem  19657  dpjidcl  19670  ablfac1b  19682  pgpfac1lem1  19686  gsummgp0  19856  isirred  19950  irredrmul  19958  isdrng2  20010  isdrngd  20025  cntzsdrg  20079  lcomfsupp  20172  lbspropd  20370  lspsneq  20393  lsppratlem6  20423  lbsextlem2  20430  lbsextlem4  20432  ringelnzr  20546  xrs1mnd  20645  xrs10  20646  xrs1cmn  20647  cnsubrg  20667  psgnodpm  20802  zrhpsgnodpm  20806  evpmodpmf1o  20810  uvcresum  21009  frlmssuvc1  21010  frlmsslsp  21012  frlmup2  21015  lindfrn  21037  f1lindf  21038  lindfmm  21043  islindf4  21054  psrbaglesupp  21136  psrbaglesuppOLD  21137  psrlidm  21181  psrridm  21182  mplsubglem  21214  mpllsslem  21215  mplsubrglem  21219  mplmonmul  21246  mplcoe1  21247  mplcoe5  21250  mplbas2  21252  evlslem3  21299  mhpvscacl  21353  coe1tmmul2  21456  coe1tmmul  21457  dmatmul  21655  1marepvsma1  21741  mdetdiaglem  21756  mdetrlin  21760  mdetrsca  21761  mdetralt  21766  maducoeval2  21798  madugsum  21801  symgmatr01  21812  gsummatr01lem3  21815  gsummatr01lem4  21816  gsummatr01  21817  smadiadetlem0  21819  smadiadetlem1a  21821  cmpfi  22568  2ndcdisj2  22617  elptr2  22734  ptcnplem  22781  xkopt  22815  kqdisj  22892  fin1aufil  23092  ptcmplem2  23213  ptcmplem3  23214  ptcmplem4  23215  opnsubg  23268  lpbl  23668  blcld  23670  zcld  23985  recld2  23986  reconnlem1  23998  divcn  24040  iundisj  24721  mbfeqalem1  24814  itg1val2  24857  itg1ge0  24859  i1fmullem  24867  i1fadd  24868  itg1addlem4  24872  itg1addlem4OLD  24873  itg1mulc  24878  itg1lea  24886  itg1le  24887  mbfi1fseqlem4  24892  itg2uba  24917  itg2lea  24918  itg2eqa  24919  itg2splitlem  24922  itg2split  24923  itgeqa  24987  ellimc3  25052  dvaddbr  25111  dvmulbr  25112  dvcobr  25119  dvcjbr  25122  dvrec  25128  dvrecg  25146  dvcnvlem  25149  dvexp3  25151  dveflem  25152  tdeglem4  25233  tdeglem4OLD  25234  deg1n0ima  25263  deg1mul3le  25290  ig1peu  25345  ply1termlem  25373  plypf1  25382  plyaddlem1  25383  plymullem1  25384  coeeulem  25394  coeidlem  25407  coeid3  25410  coefv0  25418  coemulhi  25424  coemulc  25425  dvply1  25453  fta1  25477  vieta1lem2  25480  elaa  25485  elqaalem2  25489  aannenlem2  25498  aaliou2  25509  tayl0  25530  dvtaylp  25538  taylthlem1  25541  taylthlem2  25542  pserdvlem2  25596  logbcl  25926  relogbreexp  25934  relogbcxp  25944  cxplogb  25945  dcubic  26005  rlimcnp  26124  jensen  26147  dmgmaddn0  26181  dmlogdmgm  26182  lgamgulmlem2  26188  igamz  26206  gamp1  26216  regamcl  26219  wilthlem2  26227  basellem3  26241  chpub  26377  logexprlim  26382  lgslem1  26454  lgslem4  26457  lgsvalmod  26473  lgsqr  26508  lgsqrmod  26509  lgsqrmodndvds  26510  gausslemma2dlem0b  26514  gausslemma2dlem0c  26515  gausslemma2dlem0i  26521  gausslemma2dlem1a  26522  gausslemma2dlem4  26526  gausslemma2dlem5a  26527  gausslemma2dlem7  26530  gausslemma2d  26531  lgsquad2  26543  m1lgs  26545  2lgsoddprm  26573  2sqreultblem  26605  dchrisum0fno1  26668  rplogsum  26684  ishpg  27129  elntg2  27362  umgrislfupgrlem  27501  usgruspgrb  27560  nbumgrvtx  27722  nbupgrres  27740  isuvtx  27771  cusgrexilem2  27818  cusgrexi  27819  structtocusgr  27822  cusgrres  27824  cusgrfilem2  27832  vtxdginducedm1  27919  cusconngr  28564  2pthfrgr  28657  frgrncvvdeq  28682  frgrwopreglem4  28688  frgrwopreglem5  28694  frgrwopreg  28696  frgrhash2wsp  28705  strlem1  30621  strlem3  30624  strlem4  30625  strlem5  30626  hstrlem3  30632  hstrlem4  30633  iundisjf  30937  suppss3  31068  iundisjfi  31126  qtophaus  31795  elzdif0  31939  ind0  31995  measvunilem  32189  sibfof  32316  eulerpartlemb  32344  eulerpartlemf  32346  sseqf  32368  ballotlem5  32475  ballotlemi1  32478  ballotlemii  32479  ballotlemic  32482  ballotlem1c  32483  ballotlemscr  32494  ballotlemro  32498  ballotlemfg  32501  ballotlemfrc  32502  ballotlemfrceq  32504  ballotlemrinv0  32508  plymulx0  32535  signstfvn  32557  signsvfn  32570  bnj923  32757  bnj570  32894  bnj594  32901  subfacp1lem1  33150  satffunlem2lem1  33375  mrsubcn  33490  mrsubco  33492  circum  33641  dfon2lem6  33773  xpord2pred  33801  neibastop1  34557  bj-restn0b  35271  lindsadd  35779  lindsenlbs  35781  matunitlindflem1  35782  poimirlem24  35810  poimirlem25  35811  dvtan  35836  itg2addnclem2  35838  ftc1cnnc  35858  dvasin  35870  dvreasin  35872  dvreacos  35873  isdrngo2  36125  isdrngo3  36126  divrngidl  36195  isfldidl  36235  pridlc2  36239  pridlc3  36240  prter2  36902  lsateln0  37016  lsatlss  37017  lsmsat  37029  lsatcv0  37052  lsat0cv  37054  lcv1  37062  l1cvpat  37075  dih1dimatlem  39350  dihatexv2  39360  djhcvat42  39436  dihjat1lem  39449  dochsatshp  39472  lcfl6  39521  mapdrvallem2  39666  mapdpglem32  39726  sticksstones22  40131  isdomn4  40179  evlsbagval  40282  prjspertr  40451  prjsperref  40452  prjspersym  40453  prjspvs  40456  prjsprellsp  40457  prjcrv0  40477  dffltz  40478  irrapx1  40657  pell1234qrne0  40682  pell1234qrreccl  40683  pell1234qrmulcl  40684  pell14qrgt0  40688  pell1234qrdich  40690  pell14qrdich  40698  pell1qrge1  40699  pell1qr1  40700  pell1qrgap  40703  pell14qrgapw  40705  pellqrexplicit  40706  pellqrex  40708  pellfundge  40711  pellfundgt1  40712  setindtr  40853  kelac1  40895  mpaaeu  40982  flcidc  41006  deg1mhm  41039  minregex2  41149  radcnvrat  41939  binomcxplemdvbinom  41978  disjiun2  42613  fiiuncl  42620  disjf1o  42736  difmapsn  42759  supminfxr2  43016  icoiccdif  43069  iccdificc  43084  fsumnncl  43120  fsumsupp0  43126  fprod0  43144  climrec  43151  islpcn  43187  lptre2pt  43188  limclner  43199  cnrefiisplem  43377  fprodcncf  43448  fperdvper  43467  dvdivcncf  43475  dvnmul  43491  dvmptfprodlem  43492  dvnprodlem2  43495  stoweidlem25  43573  stoweidlem28  43576  stoweidlem41  43589  stoweidlem44  43592  stoweidlem46  43594  stirlinglem5  43626  dirkercncflem1  43651  dirkercncflem2  43652  fourierdlem24  43679  fourierdlem62  43716  fouriersw  43779  fouriercn  43780  elaa2lem  43781  elaa2  43782  etransclem25  43807  etransclem35  43817  etransclem44  43826  sge0iunmptlemfi  43958  sge0fodjrnlem  43961  iundjiunlem  44004  meadjiunlem  44010  meaiininclem  44031  isomenndlem  44075  hsphoidmvle2  44130  hsphoidmvle  44131  hoidmv1lelem2  44137  hoidmvle  44145  ovnhoilem1  44146  hspdifhsp  44161  hspmbllem2  44172  ovnsubadd2lem  44190  ovolval4lem1  44194  preimagelt  44244  preimalegt  44245  fsummsndifre  44835  fsummmodsndifre  44837  odz2prm2pw  45026  fmtnoprmfac1lem  45027  fmtnoprmfac2lem1  45029  2pwp1prm  45052  lighneallem2  45069  lighneallem3  45070  lighneallem4  45073  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  bgoldbtbndlem4  45271  bgoldbtbnd  45272  c0rhm  45481  c0rnghm  45482  zrrnghm  45486  2zrngnmlid2  45520  zrinitorngc  45569  zrtermorngc  45570  mgpsumunsn  45708  mgpsumz  45709  mgpsumn  45710  lindslinindsimp1  45809  lindslinindsimp2  45815  lincresunit1  45829  lincresunit2  45830  lincresunit3lem1  45831  lincresunit3lem2  45832  lincresunit3  45833  lindssnlvec  45838  logcxp0  45892  relogbmulbexp  45918  relogbdivb  45919  dignn0fr  45958  rrxlinesc  46092  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095