MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eldifi Structured version   Unicode version

Theorem eldifi 3609
Description: Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
eldifi  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )

Proof of Theorem eldifi
StepHypRef Expression
1 eldif 3469 . 2  |-  ( A  e.  ( B  \  C )  <->  ( A  e.  B  /\  -.  A  e.  C ) )
21simplbi 460 1  |-  ( A  e.  ( B  \  C )  ->  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    e. wcel 1802    \ cdif 3456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-dif 3462
This theorem is referenced by:  difss  3614  noel  3772  tz7.7  4891  xpdifid  5422  tfi  6670  peano5  6705  tz7.48-1  7107  tz7.49  7109  dif20el  7154  oaf1o  7211  oeordi  7235  oeord  7236  oecan  7237  oeword  7238  oeworde  7241  oelimcl  7248  oeeulem  7249  oeeui  7250  oaabs2  7293  boxcutc  7511  domdifsn  7599  isinf  7732  pssnn  7737  pwfilem  7813  fsuppco2  7861  fsuppcor  7862  ordtypelem7  7949  unxpwdom2  8014  inf3lem3  8047  cantnfp1lem1  8097  cantnfp1lem3  8099  cantnfp1lem1OLD  8123  cantnfp1lem3OLD  8125  infxpenc2lem1  8396  dfacacn  8521  isf32lem3  8735  isf34lem4  8757  fin67  8775  isfin7-2  8776  domtriomlem  8822  axdc2lem  8828  axdc3lem4  8833  axdc4lem  8835  ttukeylem7  8895  konigthlem  8943  fpwwe2lem13  9020  fpwwe2  9021  hashf1lem1  12480  rlimrege0  13378  rlimrecl  13379  sumrblem  13509  fsumcvg  13510  summolem2a  13513  fsumss  13523  fsumless  13586  cvgcmpce  13608  binomlem  13617  incexclem  13624  incexc  13625  isumltss  13636  rpnnen2lem10  13831  rpnnen2lem11  13832  oddprm  14213  iserodd  14233  prmreclem2  14309  prmreclem3  14310  prmreclem5  14312  4sqlem19  14355  prmlem0  14465  firest  14704  grpinvnzcl  15981  symgextfv  16314  pmtrf  16351  pmtrdifellem3  16374  sylow2alem2  16509  sylow2a  16510  efgsf  16618  efgsrel  16623  efgs1  16624  efgsfo  16628  efgredlemc  16634  gsumzaddlem  16805  gsumzadd  16806  gsumzaddlemOLD  16807  gsumzaddOLD  16808  gsumzmhm  16828  gsumzmhmOLD  16829  gsumzinvOLD  16841  gsumsubOLD  16846  gsum2d2lem  16872  dprdfadd  16931  dprdfaddOLD  16938  dprdres  16946  subgdmdprd  16952  dmdprdsplitlem  16955  dmdprdsplitlemOLD  16956  dmdprdsplit2lem  16965  dpjidcl  16978  dpjidclOLD  16985  ablfac1b  16992  pgpfac1lem1  16996  gsummgp0  17127  isirred  17219  irredrmul  17227  isdrng2  17277  isdrngd  17292  lcomfsupOLD  17420  lcomfsupp  17421  lbspropd  17616  lspsneq  17639  lsppratlem6  17669  lbsextlem2  17676  lbsextlem4  17678  ringelnzr  17785  psrbaglesupp  17888  psrbaglesuppOLD  17889  psrlidm  17927  psrlidmOLD  17928  psrridm  17929  psrridmOLD  17930  mplsubglem  17964  mpllsslem  17965  mplsubglemOLD  17966  mpllsslemOLD  17967  mplsubrglem  17971  mplsubrglemOLD  17972  mplmonmul  17997  mplcoe1  17998  mplcoe5  18002  mplcoe2OLD  18004  mplbas2  18005  mplbas2OLD  18006  evlslem3  18054  coe1tmmul2  18188  coe1tmmul  18189  xrs1mnd  18327  xrs10  18328  xrs1cmn  18329  cnsubrg  18349  psgnodpm  18494  zrhpsgnodpm  18498  evpmodpmf1o  18502  uvcresum  18694  frlmssuvc1  18695  frlmssuvc1OLD  18697  frlmsslsp  18699  frlmsslspOLD  18700  frlmup2  18703  lindfrn  18726  f1lindf  18727  lindfmm  18732  islindf4  18743  dmatmul  18869  1marepvsma1  18955  mdetdiaglem  18970  mdetrlin  18974  mdetrsca  18975  mdetralt  18980  maducoeval2  19012  madugsum  19015  symgmatr01  19026  gsummatr01lem3  19029  gsummatr01lem4  19030  gsummatr01  19031  smadiadetlem0  19033  smadiadetlem1a  19035  cmpfi  19778  2ndcdisj2  19828  elptr2  19945  ptcnplem  19992  xkopt  20026  kqdisj  20103  fin1aufil  20303  ptcmplem2  20423  ptcmplem3  20424  ptcmplem4  20425  opnsubg  20476  lpbl  20876  blcld  20878  zcld  21188  recld2  21189  reconnlem1  21201  divcn  21242  iundisj  21828  mbfeqalem  21919  itg1val2  21961  itg1ge0  21963  i1fmullem  21971  i1fadd  21972  itg1addlem4  21976  itg1mulc  21981  itg1lea  21989  itg1le  21990  mbfi1fseqlem4  21995  itg2uba  22020  itg2lea  22021  itg2eqa  22022  itg2splitlem  22025  itg2split  22026  itgeqa  22090  ellimc3  22153  dvaddbr  22211  dvmulbr  22212  dvcobr  22219  dvcjbr  22222  dvrec  22228  dvcnvlem  22247  dvexp3  22249  dveflem  22250  tdeglem4  22328  deg1n0ima  22359  deg1mul3le  22387  ig1peu  22442  ply1termlem  22470  plypf1  22479  plyaddlem1  22480  plymullem1  22481  coeeulem  22491  coeidlem  22504  coeid3  22507  coefv0  22514  coemulhi  22520  coemulc  22521  dvply1  22549  fta1  22573  vieta1lem2  22576  elaa  22581  elqaalem2  22585  aannenlem2  22594  aaliou2  22605  tayl0  22626  dvtaylp  22634  taylthlem1  22637  taylthlem2  22638  pserdvlem2  22692  dcubic  23046  rlimcnp  23164  jensen  23187  wilthlem2  23212  basellem3  23225  chpub  23364  logexprlim  23369  lgslem1  23440  lgslem4  23443  lgsvalmod  23459  lgsqr  23490  lgsquadlem1  23498  lgsquad2  23504  m1lgs  23506  dchrisum0fno1  23565  rplogsum  23581  ishpg  23997  cusgraexi  24337  uvtxnbgra  24362  cusconngra  24545  frgrancvvdeqlem9  24910  frgrancvvdeq  24911  frgrancvvdgeq  24912  2spotiundisj  24931  frghash2spot  24932  ablomul  25226  mulid  25227  zerdivemp1  25305  strlem1  27038  strlem3  27041  strlem4  27042  strlem5  27043  hstrlem3  27049  hstrlem4  27050  iundisjf  27317  suppss3  27419  iundisjfi  27470  qtophaus  27709  elzdif0  27831  logbcl  27883  ind0  27903  measvunilem  28053  sibfof  28152  eulerpartlemb  28177  eulerpartlemf  28179  sseqf  28201  ballotlem5  28308  ballotlemi1  28311  ballotlemii  28312  ballotlemic  28315  ballotlem1c  28316  ballotlemscr  28327  ballotlemro  28331  ballotlemfg  28334  ballotlemfrc  28335  ballotlemfrceq  28337  ballotlemrinv0  28341  plymulx0  28374  signstfvn  28396  dmgmaddn0  28435  dmlogdmgm  28436  lgamgulmlem2  28442  igamz  28460  gamp1  28470  regamcl  28473  subfacp1lem1  28493  mrsubcn  28749  mrsubco  28751  circum  28910  prodrblem  29033  fprodcvg  29034  prodmolem2a  29038  fprodss  29052  dfon2lem6  29192  wfrlem10  29324  wfrlem15  29329  dvtan  30037  itg2addnclem2  30039  ftc1cnnc  30061  dvasin  30075  dvreasin  30077  dvreacos  30078  neibastop1  30149  isdrngo2  30333  isdrngo3  30334  divrngidl  30397  isfldidl  30437  pridlc2  30441  pridlc3  30442  prter2  30594  irrapx1  30736  pell1234qrne0  30761  pell1234qrreccl  30762  pell1234qrmulcl  30763  pell14qrgt0  30767  pell1234qrdich  30769  pell14qrdich  30777  pell1qrge1  30778  pell1qr1  30779  pell1qrgap  30782  pell14qrgapw  30784  pellqrexplicit  30785  pellqrex  30787  pellfundge  30790  pellfundgt1  30791  setindtr  30938  kelac1  30981  mpaaeu  31072  flcidc  31096  cntzsdrg  31124  deg1mhm  31140  radcnvrat  31168  icoiccdif  31500  climrec  31517  islpcn  31553  lptre2pt  31554  limclner  31565  dvrecg  31611  fperdvper  31619  dvdivcncf  31628  stoweidlem25  31696  stoweidlem28  31699  stoweidlem41  31712  stoweidlem44  31715  stoweidlem46  31717  stirlinglem5  31749  dirkercncflem1  31774  dirkercncflem2  31775  fourierdlem24  31802  fourierdlem62  31840  fouriersw  31903  fouriercn  31904  fsummsndifre  32183  fsummmodsndifre  32185  2zrngnmlid2  32464  mgpsumunsn  32679  mgpsumz  32680  mgpsumn  32681  lindslinindsimp1  32788  lindslinindsimp2  32794  lincresunit1  32808  lincresunit2  32809  lincresunit3lem1  32810  lincresunit3lem2  32811  lincresunit3  32812  lindssnlvec  32817  elogb  32899  bnj923  33554  bnj570  33691  bnj594  33698  lsateln0  34443  lsatlss  34444  lsmsat  34456  lsatcv0  34479  lsat0cv  34481  lcv1  34489  l1cvpat  34502  dih1dimatlem  36779  dihatexv2  36789  djhcvat42  36865  dihjat1lem  36878  dochsatshp  36901  lcfl6  36950  mapdrvallem2  37095  mapdpglem32  37155
  Copyright terms: Public domain W3C validator