Theorem elssuni 4003

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

Step	Hyp	Ref	Expression
1		ssid 3327	. 2 |- A C_ A
2		ssuni 3997	. 2 |- ( ( A C_ A /\ A e. B ) -> A C_ U. B )
3	1, 2	mpan 652	1 |- ( A e. B -> A C_ U. B )

Syntax hints:   -> wi 4   e. wcel 1721   C_ wss 3280   U.cuni 3975

This theorem is referenced by:  unissel  4004  ssunieq  4008  pwuni  4355  pwel  4375  uniopel  4420  iunpw  4718  dmrnssfld  5088  unixp0  5362  fvssunirn  5713  sorpssuni  6490  pwuninel2  6503  onfununi  6562  tfrlem9  6605  tfrlem9a  6606  tfrlem13  6610  sbthlem1  7176  sbthlem2  7177  2pwuninel  7221  ordunifi  7316  unifpw  7367  fissuni  7369  dffi3  7394  cantnfp1lem3  7592  oemapvali  7596  cantnflem1  7601  cnfcom3lem  7616  rankuni2b  7735  carduni  7824  r0weon  7850  dfac8clem  7869  cardinfima  7934  alephfp  7945  iunfictbso  7951  dfac5lem4  7963  dfac2a  7966  dfacacn  7977  dfac12lem2  7980  kmlem2  7987  fin23lem16  8171  fin23lem21  8175  isf32lem5  8193  fin1a2lem11  8246  fin1a2lem13  8248  itunitc  8257  axdc2lem  8284  axdc3lem2  8287  ttukeylem5  8349  ttukeylem6  8350  fpwwe2lem11  8471  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwe2  8474  wunex2  8569  inatsk  8609  tskuni  8614  suplem1pr  8885  suplem2pr  8886  unirnioo  10960  mrcuni  13801  isacs3lem  14547  mrelatlub  14567  dprd2dlem1  15554  lbsextlem2  16186  eltopss  16935  toponss  16949  isbasis3g  16969  baspartn  16974  bastg  16986  tgcl  16989  fctop  17023  cctop  17025  ppttop  17026  epttop  17028  difopn  17053  ssntr  17077  isopn3  17085  isopn3i  17101  toponmre  17112  neiuni  17141  neiptoptop  17150  resttopon  17179  restopn2  17195  perfopn  17203  pnfnei  17238  mnfnei  17239  ssidcn  17273  lmcnp  17322  pnrmopn  17361  ist1-2  17365  nrmsep  17375  isnrm2  17376  isnrm3  17377  regsep2  17394  cncmp  17409  hauscmplem  17423  hauscmp  17424  conndisj  17432  cnconn  17438  concompss  17449  islly2  17500  nllyrest  17502  nllyidm  17505  hausllycmp  17510  cldllycmp  17511  lly1stc  17512  kgentopon  17523  kgenss  17528  llycmpkgen2  17535  1stckgen  17539  txuni2  17550  ptpjpre1  17556  ptuni2  17561  ptbasfi  17566  xkouni  17584  txcnpi  17593  ptpjopn  17597  txindis  17619  txnlly  17622  txtube  17625  hausdiag  17630  xkopt  17640  xkococnlem  17644  txcon  17674  qtopuni  17687  qtopkgen  17695  tgqtop  17697  regr1lem  17724  kqreglem1  17726  kqreglem2  17727  kqnrmlem1  17728  kqnrmlem2  17729  hmeoimaf1o  17755  reghmph  17778  nrmhmph  17779  filcon  17868  trfil1  17871  ufildr  17916  flimfil  17954  flimfnfcls  18013  alexsublem  18028  alexsubALTlem3  18033  ustbas2  18208  tgioo  18780  xrtgioo  18790  xrsmopn  18796  opnreen  18815  cnheibor  18933  cnllycmp  18934  lebnumlem1  18939  lebnumlem3  18941  bcthlem5  19234  bcth3  19237  voliunlem1  19397  voliunlem3  19399  volsup  19403  opnmbllem  19446  mbfimaopnlem  19500  lhop  19853  ubthlem1  22325  shatomistici  23817  hatomistici  23818  tpr2rico  24263  hasheuni  24428  difelsiga  24469  prob01  24624  probdsb  24633  totprobd  24637  probmeasb  24641  cndprobtot  24647  orvcelval  24679  pconcon  24871  cvmsf1o  24912  cvmscld  24913  cvmsss2  24914  cvmopnlem  24918  cvmfolem  24919  cvmliftmolem1  24921  cvmliftlem6  24930  cvmliftlem8  24932  cvmlift2lem9  24951  cvmlift2lem11  24953  cvmlift2lem12  24954  cvmlift3lem6  24964  dfon2lem3  25355  dfon2lem7  25359  trpredpred  25445  wfrlem12  25481  wfrlem16  25485  frrlem11  25507  nobndlem2  25561  nobndlem8  25567  nofulllem3  25572  nofulllem5  25574  mblfinlem  26143  mbfresfi  26152  ntruni  26220  clsint2  26222  comppfsc  26277  neibastop1  26278  topmeet  26283  topjoin  26284  fnemeet1  26285  fnejoin1  26287  heiborlem1  26410  isnacs3  26654  aomclem4  27022  kelac2  27031  stoweidlem28  27644  stoweidlem50  27666  stoweidlem52  27668  stoweidlem53  27669  stoweidlem54  27670  bnj1450  29125  bnj1501  29142  lssats  29495  dicval  31659  mapdunirnN  32133

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294  df-uni 3976