Theorem eldifi 3732

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 1990   ∖ cdif 3571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577

This theorem is referenced by:  difss  3737  noel  3919  eqoreldif  4225  eqoreldifOLD  4226  xpdifid  5562  tz7.7  5749  tfi  7053  peano5  7089  wfrlem10  7424  wfrlem15  7429  tz7.48-1  7538  tz7.49  7540  dif20el  7585  oaf1o  7643  oeordi  7667  oeord  7668  oecan  7669  oeword  7670  oeworde  7673  oelimcl  7680  oeeulem  7681  oeeui  7682  oaabs2  7725  boxcutc  7951  domdifsn  8043  isinf  8173  pssnn  8178  pwfilem  8260  fsuppco2  8308  fsuppcor  8309  ordtypelem7  8429  unxpwdom2  8493  inf3lem3  8527  cantnfp1lem1  8575  cantnfp1lem3  8577  infxpenc2lem1  8842  dfacacn  8963  isf32lem3  9177  isf34lem4  9199  fin67  9217  isfin7-2  9218  domtriomlem  9264  axdc2lem  9270  axdc3lem4  9275  axdc4lem  9277  ttukeylem7  9337  konigthlem  9390  fpwwe2lem13  9464  fpwwe2  9465  modfzo0difsn  12742  hashf1lem1  13239  hashle2prv  13260  rlimrege0  14310  rlimrecl  14311  sumrblem  14442  fsumcvg  14443  summolem2a  14446  fsumss  14456  fsumless  14528  cvgcmpce  14550  binomlem  14561  incexclem  14568  incexc  14569  isumltss  14580  prodrblem  14659  fprodcvg  14660  prodmolem2a  14664  fprodss  14678  fprodn0f  14722  fprodeq0g  14725  fprodmodd  14728  rpnnen2lem10  14952  rpnnen2lem11  14953  sumeven  15110  sumodd  15111  lcmfunsnlem2  15353  oddprmge3  15412  oddprm  15515  nnoddn2prm  15516  nnoddn2prmb  15518  iserodd  15540  prmreclem2  15621  prmreclem3  15622  prmreclem5  15624  4sqlem19  15667  prmdvdsprmo  15746  prmodvdslcmf  15751  prmlem0  15812  firest  16093  grpinvnzcl  17487  symgextfv  17838  pmtrf  17875  pmtrdifellem3  17898  sylow2alem2  18033  sylow2a  18034  efgsf  18142  efgsrel  18147  efgs1  18148  efgsfo  18152  efgredlemc  18158  gsumzaddlem  18321  gsumzadd  18322  gsumzmhm  18337  gsum2d2lem  18372  dprdfadd  18419  dprdres  18427  subgdmdprd  18433  dmdprdsplitlem  18436  dmdprdsplit2lem  18444  dpjidcl  18457  ablfac1b  18469  pgpfac1lem1  18473  gsummgp0  18608  isirred  18699  irredrmul  18707  isdrng2  18757  isdrngd  18772  lcomfsupp  18903  lbspropd  19099  lspsneq  19122  lsppratlem6  19152  lbsextlem2  19159  lbsextlem4  19161  ringelnzr  19266  psrbaglesupp  19368  psrlidm  19403  psrridm  19404  mplsubglem  19434  mpllsslem  19435  mplsubrglem  19439  mplmonmul  19464  mplcoe1  19465  mplcoe5  19468  mplbas2  19470  evlslem3  19514  coe1tmmul2  19646  coe1tmmul  19647  xrs1mnd  19784  xrs10  19785  xrs1cmn  19786  cnsubrg  19806  psgnodpm  19934  zrhpsgnodpm  19938  evpmodpmf1o  19942  uvcresum  20132  frlmssuvc1  20133  frlmsslsp  20135  frlmup2  20138  lindfrn  20160  f1lindf  20161  lindfmm  20166  islindf4  20177  dmatmul  20303  1marepvsma1  20389  mdetdiaglem  20404  mdetrlin  20408  mdetrsca  20409  mdetralt  20414  maducoeval2  20446  madugsum  20449  symgmatr01  20460  gsummatr01lem3  20463  gsummatr01lem4  20464  gsummatr01  20465  smadiadetlem0  20467  smadiadetlem1a  20469  cmpfi  21211  2ndcdisj2  21260  elptr2  21377  ptcnplem  21424  xkopt  21458  kqdisj  21535  fin1aufil  21736  ptcmplem2  21857  ptcmplem3  21858  ptcmplem4  21859  opnsubg  21911  lpbl  22308  blcld  22310  zcld  22616  recld2  22617  reconnlem1  22629  divcn  22671  iundisj  23316  mbfeqalem  23409  itg1val2  23451  itg1ge0  23453  i1fmullem  23461  i1fadd  23462  itg1addlem4  23466  itg1mulc  23471  itg1lea  23479  itg1le  23480  mbfi1fseqlem4  23485  itg2uba  23510  itg2lea  23511  itg2eqa  23512  itg2splitlem  23515  itg2split  23516  itgeqa  23580  ellimc3  23643  dvaddbr  23701  dvmulbr  23702  dvcobr  23709  dvcjbr  23712  dvrec  23718  dvrecg  23736  dvcnvlem  23739  dvexp3  23741  dveflem  23742  tdeglem4  23820  deg1n0ima  23849  deg1mul3le  23876  ig1peu  23931  ply1termlem  23959  plypf1  23968  plyaddlem1  23969  plymullem1  23970  coeeulem  23980  coeidlem  23993  coeid3  23996  coefv0  24004  coemulhi  24010  coemulc  24011  dvply1  24039  fta1  24063  vieta1lem2  24066  elaa  24071  elqaalem2  24075  aannenlem2  24084  aaliou2  24095  tayl0  24116  dvtaylp  24124  taylthlem1  24127  taylthlem2  24128  pserdvlem2  24182  logbcl  24505  relogbreexp  24513  relogbcxp  24523  cxplogb  24524  dcubic  24573  rlimcnp  24692  jensen  24715  dmgmaddn0  24749  dmlogdmgm  24750  lgamgulmlem2  24756  igamz  24774  gamp1  24784  regamcl  24787  wilthlem2  24795  basellem3  24809  chpub  24945  logexprlim  24950  lgslem1  25022  lgslem4  25025  lgsvalmod  25041  lgsqr  25076  lgsqrmod  25077  lgsqrmodndvds  25078  gausslemma2dlem0b  25082  gausslemma2dlem0c  25083  gausslemma2dlem0i  25089  gausslemma2dlem1a  25090  gausslemma2dlem4  25094  gausslemma2dlem5a  25095  gausslemma2dlem7  25098  gausslemma2d  25099  lgsquadlem1  25105  lgsquad2  25111  m1lgs  25113  2lgsoddprm  25141  dchrisum0fno1  25200  rplogsum  25216  ishpg  25651  umgrislfupgrlem  26017  usgruspgrb  26076  nbumgrvtx  26242  nbupgrres  26266  isuvtxa  26295  cusgrexilem2  26338  cusgrexi  26339  structtocusgr  26342  cusgrres  26344  cusgrfilem2  26352  vtxdginducedm1  26439  cusconngr  27051  2pthfrgr  27148  frgrncvvdeq  27173  frgrwopreglem4  27179  frgrwopreglem5  27185  frgrwopreg  27187  frgrhash2wsp  27196  strlem1  29109  strlem3  29112  strlem4  29113  strlem5  29114  hstrlem3  29120  hstrlem4  29121  iundisjf  29402  suppss3  29502  iundisjfi  29555  qtophaus  29903  elzdif0  30024  ind0  30080  measvunilem  30275  sibfof  30402  eulerpartlemb  30430  eulerpartlemf  30432  sseqf  30454  ballotlem5  30561  ballotlemi1  30564  ballotlemii  30565  ballotlemic  30568  ballotlem1c  30569  ballotlemscr  30580  ballotlemro  30584  ballotlemfg  30587  ballotlemfrc  30588  ballotlemfrceq  30590  ballotlemrinv0  30594  plymulx0  30624  signstfvn  30646  bnj923  30838  bnj570  30975  bnj594  30982  subfacp1lem1  31161  mrsubcn  31416  mrsubco  31418  circum  31568  dfon2lem6  31693  neibastop1  32354  bj-restn0b  33044  lindsenlbs  33404  matunitlindflem1  33405  poimirlem24  33433  poimirlem25  33434  dvtan  33460  itg2addnclem2  33462  ftc1cnnc  33484  dvasin  33496  dvreasin  33498  dvreacos  33499  isdrngo2  33757  isdrngo3  33758  divrngidl  33827  isfldidl  33867  pridlc2  33871  pridlc3  33872  prter2  34166  lsateln0  34282  lsatlss  34283  lsmsat  34295  lsatcv0  34318  lsat0cv  34320  lcv1  34328  l1cvpat  34341  dih1dimatlem  36618  dihatexv2  36628  djhcvat42  36704  dihjat1lem  36717  dochsatshp  36740  lcfl6  36789  mapdrvallem2  36934  mapdpglem32  36994  irrapx1  37392  pell1234qrne0  37417  pell1234qrreccl  37418  pell1234qrmulcl  37419  pell14qrgt0  37423  pell1234qrdich  37425  pell14qrdich  37433  pell1qrge1  37434  pell1qr1  37435  pell1qrgap  37438  pell14qrgapw  37440  pellqrexplicit  37441  pellqrex  37443  pellfundge  37446  pellfundgt1  37447  setindtr  37591  kelac1  37633  mpaaeu  37720  flcidc  37744  cntzsdrg  37772  deg1mhm  37785  radcnvrat  38513  binomcxplemdvbinom  38552  disjiun2  39226  fiiuncl  39234  disjf1o  39378  difmapsn  39404  supminfxr2  39699  icoiccdif  39750  iccdificc  39766  fsumnncl  39803  fsumsplit1  39804  fsumsupp0  39810  fprod0  39828  climrec  39835  islpcn  39871  lptre2pt  39872  limclner  39883  cnrefiisplem  40055  fprodcncf  40114  fperdvper  40133  dvdivcncf  40142  dvnmul  40158  dvmptfprodlem  40159  dvnprodlem2  40162  stoweidlem25  40242  stoweidlem28  40245  stoweidlem41  40258  stoweidlem44  40261  stoweidlem46  40263  stirlinglem5  40295  dirkercncflem1  40320  dirkercncflem2  40321  fourierdlem24  40348  fourierdlem62  40385  fouriersw  40448  fouriercn  40449  elaa2lem  40450  elaa2  40451  etransclem25  40476  etransclem35  40486  etransclem44  40495  sge0iunmptlemfi  40630  sge0fodjrnlem  40633  iundjiunlem  40676  meadjiunlem  40682  meaiininclem  40700  isomenndlem  40744  hsphoidmvle2  40799  hsphoidmvle  40800  hoidmv1lelem2  40806  hoidmvle  40814  ovnhoilem1  40815  hspdifhsp  40830  hspmbllem2  40841  ovnsubadd2lem  40859  ovolval4lem1  40863  preimagelt  40912  preimalegt  40913  fsummsndifre  41342  fsummmodsndifre  41344  odz2prm2pw  41475  fmtnoprmfac1lem  41476  fmtnoprmfac2lem1  41478  2pwp1prm  41503  lighneallem2  41523  lighneallem3  41524  lighneallem4  41527  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  bgoldbtbndlem4  41696  bgoldbtbnd  41697  c0rhm  41912  c0rnghm  41913  zrrnghm  41917  2zrngnmlid2  41951  zrinitorngc  42000  zrtermorngc  42001  mgpsumunsn  42140  mgpsumz  42141  mgpsumn  42142  lindslinindsimp1  42246  lindslinindsimp2  42252  lincresunit1  42266  lincresunit2  42267  lincresunit3lem1  42268  lincresunit3lem2  42269  lincresunit3  42270  lindssnlvec  42275  logcxp0  42329  relogbmulbexp  42355  relogbdivb  42356  dignn0fr  42395