Theorem elssuni 4241

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 3463	. 2 |- A C_ A
2		ssuni 4234	. 2 |- ( ( A C_ A /\ A e. B ) -> A C_ U. B )
3	1, 2	mpan 681	1 |- ( A e. B -> A C_ U. B )

Syntax hints:   -> wi 4   e. wcel 1898   C_ wss 3416   U.cuni 4212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-in 3423  df-ss 3430  df-uni 4213

This theorem is referenced by:  unissel  4242  ssunieq  4246  pwuni  4648  pwel  4669  uniopel  4722  dmrnssfld  5115  unixp0  5393  fvssunirn  5915  sorpssuni  6612  iunpw  6637  pwuninel2  7052  wfrlem12  7078  wfrlem16  7082  wfrlem17  7083  onfununi  7091  tfrlem9  7134  tfrlem9a  7135  tfrlem13  7139  sbthlem1  7713  sbthlem2  7714  2pwuninel  7758  ordunifi  7852  unifpw  7908  fissuni  7910  dffi3  7976  cantnfp1lem3  8216  oemapvali  8220  cantnflem1  8225  cnfcom3lem  8239  rankuni2b  8355  carduni  8446  r0weon  8474  dfac8clem  8494  cardinfima  8559  alephfp  8570  iunfictbso  8576  dfac5lem4  8588  dfac2a  8591  dfacacn  8602  dfac12lem2  8605  kmlem2  8612  fin23lem16  8796  fin23lem21  8800  isf32lem5  8818  fin1a2lem11  8871  fin1a2lem13  8873  itunitc  8882  axdc2lem  8909  axdc3lem2  8912  ttukeylem5  8974  ttukeylem6  8975  fpwwe2lem11  9096  fpwwe2lem12  9097  fpwwe2lem13  9098  fpwwe2  9099  wunex2  9194  inatsk  9234  tskuni  9239  suplem1pr  9508  suplem2pr  9509  unirnioo  11768  mrcuni  15582  isacs3lem  16467  mrelatlub  16487  dprd2dlem1  17729  lbsextlem2  18437  eltopss  19992  toponss  19999  isbasis3g  20019  baspartn  20024  bastg  20036  tgcl  20040  fctop  20074  cctop  20076  ppttop  20077  epttop  20079  difopn  20104  ssntr  20128  isopn3  20137  isopn3i  20153  toponmre  20164  neiuni  20193  neiptoptop  20202  resttopon  20232  restopn2  20248  perfopn  20256  pnfnei  20291  mnfnei  20292  ssidcn  20326  lmcnp  20375  pnrmopn  20414  ist1-2  20418  nrmsep  20428  isnrm2  20429  isnrm3  20430  regsep2  20447  cncmp  20462  hauscmplem  20476  hauscmp  20477  conndisj  20486  cnconn  20492  concompss  20503  islly2  20554  nllyrest  20556  nllyidm  20559  hausllycmp  20564  cldllycmp  20565  lly1stc  20566  comppfsc  20602  kgentopon  20608  kgenss  20613  llycmpkgen2  20620  1stckgen  20624  txuni2  20635  ptpjpre1  20641  ptuni2  20646  ptbasfi  20651  xkouni  20669  txcnpi  20678  ptpjopn  20682  txindis  20704  txnlly  20707  txtube  20710  hausdiag  20715  xkopt  20725  xkococnlem  20729  txcon  20759  qtopuni  20772  qtopkgen  20780  tgqtop  20782  regr1lem  20809  kqreglem1  20811  kqreglem2  20812  kqnrmlem1  20813  kqnrmlem2  20814  hmeoimaf1o  20840  reghmph  20863  nrmhmph  20864  filcon  20953  trfil1  20956  ufildr  21001  flimfil  21039  flimfnfcls  21098  alexsublem  21114  alexsubALTlem3  21119  ustbas2  21295  tgioo  21869  xrtgioo  21879  xrsmopn  21885  opnreen  21904  cnheibor  22038  cnllycmp  22039  lebnumlem1  22044  lebnumlem3  22046  lebnumlem1OLD  22047  lebnumlem3OLD  22049  bcthlem5  22351  bcth3  22354  voliunlem1  22559  voliunlem3  22561  volsup  22565  opnmbllem  22615  mbfimaopnlem  22667  lhop  23024  tglnpt  24650  tglineintmo  24743  ubthlem1  26568  shatomistici  28070  hatomistici  28071  unifi3  28345  tpr2rico  28769  hasheuni  28957  difelsiga  29006  prob01  29296  probdsb  29305  totprobd  29309  probmeasb  29313  cndprobtot  29319  orvcelval  29351  bnj1450  29909  bnj1501  29926  pconcon  30004  cvmsf1o  30045  cvmscld  30046  cvmsss2  30047  cvmopnlem  30051  cvmfolem  30052  cvmliftmolem1  30054  cvmliftlem6  30063  cvmliftlem8  30065  cvmlift2lem9  30084  cvmlift2lem11  30086  cvmlift2lem12  30087  cvmlift3lem6  30097  dfon2lem3  30481  dfon2lem7  30485  trpredpred  30519  frrlem11  30576  nobndlem2  30632  nobndlem8  30638  nofulllem3  30643  nofulllem5  30645  ntruni  31033  clsint2  31035  neibastop1  31065  topmeet  31070  topjoin  31071  fnemeet1  31072  fnejoin1  31074  opnmbllem0  32022  mbfresfi  32033  heiborlem1  32189  lssats  32624  dicval  34790  mapdunirnN  35264  isnacs3  35598  aomclem4  35961  kelac2  35969  ssuniint  37465  stoweidlem28  37989  stoweidlem50  38012  stoweidlem52  38014  stoweidlem53  38015  stoweidlem54  38016  prsal  38280  salincl  38285  saliincl  38287  saldifcl2  38288  salexct  38294  psmeasurelem  38413  caragenuni  38440  carageniuncl  38452  caratheodorylem1  38455  caratheodorylem2  38456  voncmpl  38550