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

Theorem elssuni 3957
Description: An element of a class is a subclass of its union. Theorem 8.6 of [Quine] p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Jun-1994.)
Assertion
Ref Expression
elssuni  |-  ( A  e.  B  ->  A  C_ 
U. B )

Proof of Theorem elssuni
StepHypRef Expression
1 ssid 3283 . 2  |-  A  C_  A
2 ssuni 3951 . 2  |-  ( ( A  C_  A  /\  A  e.  B )  ->  A  C_  U. B )
31, 2mpan 651 1  |-  ( A  e.  B  ->  A  C_ 
U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1715    C_ wss 3238   U.cuni 3929
This theorem is referenced by:  unissel  3958  ssunieq  3962  pwuni  4308  pwel  4328  uniopel  4373  iunpw  4673  dmrnssfld  5041  unixp0  5309  fvssunirn  5658  sorpssuni  6428  pwuninel2  6441  onfununi  6500  tfrlem9  6543  tfrlem9a  6544  tfrlem13  6548  sbthlem1  7114  sbthlem2  7115  2pwuninel  7159  ordunifi  7254  unifpw  7305  fissuni  7307  dffi3  7331  cantnfp1lem3  7529  oemapvali  7533  cantnflem1  7538  cnfcom3lem  7553  rankuni2b  7672  carduni  7761  r0weon  7787  dfac8clem  7806  cardinfima  7871  alephfp  7882  iunfictbso  7888  dfac5lem4  7900  dfac2a  7903  dfacacn  7914  dfac12lem2  7917  kmlem2  7924  fin23lem16  8108  fin23lem21  8112  isf32lem5  8130  fin1a2lem11  8183  fin1a2lem13  8185  itunitc  8194  axdc2lem  8221  axdc3lem2  8224  ttukeylem5  8287  ttukeylem6  8288  fpwwe2lem11  8409  fpwwe2lem12  8410  fpwwe2lem13  8411  fpwwe2  8412  wunex2  8507  inatsk  8547  tskuni  8552  suplem1pr  8823  suplem2pr  8824  unirnioo  10896  mrcuni  13733  isacs3lem  14479  mrelatlub  14499  dprd2dlem1  15486  lbsextlem2  16122  eltopss  16870  toponss  16884  isbasis3g  16904  baspartn  16909  bastg  16921  tgcl  16924  fctop  16958  cctop  16960  ppttop  16961  epttop  16963  difopn  16988  ssntr  17012  isopn3  17020  isopn3i  17036  toponmre  17047  neiuni  17076  resttopon  17109  restopn2  17125  perfopn  17132  pnfnei  17167  mnfnei  17168  ssidcn  17202  lmcnp  17249  pnrmopn  17288  ist1-2  17292  nrmsep  17302  isnrm2  17303  isnrm3  17304  regsep2  17321  cncmp  17336  hauscmplem  17350  hauscmp  17351  conndisj  17359  cnconn  17365  concompss  17376  islly2  17427  nllyrest  17429  nllyidm  17432  hausllycmp  17437  cldllycmp  17438  lly1stc  17439  kgentopon  17450  kgenss  17455  llycmpkgen2  17462  1stckgen  17466  txuni2  17477  ptpjpre1  17483  ptuni2  17488  ptbasfi  17493  xkouni  17511  txcnpi  17519  ptpjopn  17523  txindis  17545  txnlly  17548  txtube  17551  hausdiag  17556  xkopt  17566  xkococnlem  17570  txcon  17600  qtopuni  17610  qtopkgen  17618  tgqtop  17620  regr1lem  17647  kqreglem1  17649  kqreglem2  17650  kqnrmlem1  17651  kqnrmlem2  17652  hmeoimaf1o  17678  reghmph  17701  nrmhmph  17702  filcon  17791  trfil1  17794  ufildr  17839  flimfil  17877  flimfnfcls  17936  alexsublem  17951  alexsubALTlem3  17956  tgioo  18515  xrtgioo  18525  xrsmopn  18531  opnreen  18550  cnheibor  18668  cnllycmp  18669  lebnumlem1  18674  lebnumlem3  18676  bcthlem5  18965  bcth2  18967  bcth3  18968  voliunlem1  19122  voliunlem3  19124  volsup  19128  opnmbllem  19171  mbfimaopnlem  19225  lhop  19578  ubthlem1  21762  shatomistici  23254  hatomistici  23255  neiptoptop  23643  tpr2rico  23665  ustbas2  23728  hasheuni  23940  prob01  24119  probdsb  24128  totprobd  24132  probmeasb  24136  cndprobtot  24142  orvcelval  24174  pconcon  24365  cvmsf1o  24406  cvmscld  24407  cvmsss2  24408  cvmopnlem  24412  cvmfolem  24413  cvmliftmolem1  24415  cvmliftlem6  24424  cvmliftlem8  24426  cvmlift2lem9  24445  cvmlift2lem11  24447  cvmlift2lem12  24448  cvmlift3lem6  24458  dfon2lem3  24882  dfon2lem7  24886  trpredpred  24972  wfrlem12  25008  wfrlem16  25012  frrlem11  25034  nobndlem2  25088  nobndlem8  25094  nofulllem3  25099  nofulllem5  25101  ntruni  25752  clsint2  25754  comppfsc  25814  neibastop1  25815  topmeet  25820  topjoin  25821  fnemeet1  25822  fnejoin1  25824  heiborlem1  26041  isnacs3  26291  aomclem4  26660  kelac2  26669  stoweidlem28  27283  stoweidlem50  27305  stoweidlem52  27307  stoweidlem53  27308  stoweidlem54  27309  bnj1450  28844  bnj1501  28861  lssats  29273  dicval  31437  mapdunirnN  31911
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-v 2875  df-in 3245  df-ss 3252  df-uni 3930
  Copyright terms: Public domain W3C validator