Theorem elssuni 4248

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

Syntax hints:   -> wi 4   e. wcel 1872   C_ wss 3436   U.cuni 4219

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-in 3443  df-ss 3450  df-uni 4220

This theorem is referenced by:  unissel  4249  ssunieq  4253  pwuni  4652  pwel  4673  uniopel  4724  dmrnssfld  5112  unixp0  5389  fvssunirn  5904  sorpssuni  6594  iunpw  6619  pwuninel2  7032  wfrlem12  7058  wfrlem16  7062  wfrlem17  7063  onfununi  7071  tfrlem9  7114  tfrlem9a  7115  tfrlem13  7119  sbthlem1  7691  sbthlem2  7692  2pwuninel  7736  ordunifi  7830  unifpw  7886  fissuni  7888  dffi3  7954  cantnfp1lem3  8193  oemapvali  8197  cantnflem1  8202  cnfcom3lem  8216  rankuni2b  8332  carduni  8423  r0weon  8451  dfac8clem  8470  cardinfima  8535  alephfp  8546  iunfictbso  8552  dfac5lem4  8564  dfac2a  8567  dfacacn  8578  dfac12lem2  8581  kmlem2  8588  fin23lem16  8772  fin23lem21  8776  isf32lem5  8794  fin1a2lem11  8847  fin1a2lem13  8849  itunitc  8858  axdc2lem  8885  axdc3lem2  8888  ttukeylem5  8950  ttukeylem6  8951  fpwwe2lem11  9072  fpwwe2lem12  9073  fpwwe2lem13  9074  fpwwe2  9075  wunex2  9170  inatsk  9210  tskuni  9215  suplem1pr  9484  suplem2pr  9485  unirnioo  11741  mrcuni  15526  isacs3lem  16411  mrelatlub  16431  dprd2dlem1  17673  lbsextlem2  18381  eltopss  19935  toponss  19942  isbasis3g  19962  baspartn  19967  bastg  19979  tgcl  19983  fctop  20017  cctop  20019  ppttop  20020  epttop  20022  difopn  20047  ssntr  20071  isopn3  20080  isopn3i  20096  toponmre  20107  neiuni  20136  neiptoptop  20145  resttopon  20175  restopn2  20191  perfopn  20199  pnfnei  20234  mnfnei  20235  ssidcn  20269  lmcnp  20318  pnrmopn  20357  ist1-2  20361  nrmsep  20371  isnrm2  20372  isnrm3  20373  regsep2  20390  cncmp  20405  hauscmplem  20419  hauscmp  20420  conndisj  20429  cnconn  20435  concompss  20446  islly2  20497  nllyrest  20499  nllyidm  20502  hausllycmp  20507  cldllycmp  20508  lly1stc  20509  comppfsc  20545  kgentopon  20551  kgenss  20556  llycmpkgen2  20563  1stckgen  20567  txuni2  20578  ptpjpre1  20584  ptuni2  20589  ptbasfi  20594  xkouni  20612  txcnpi  20621  ptpjopn  20625  txindis  20647  txnlly  20650  txtube  20653  hausdiag  20658  xkopt  20668  xkococnlem  20672  txcon  20702  qtopuni  20715  qtopkgen  20723  tgqtop  20725  regr1lem  20752  kqreglem1  20754  kqreglem2  20755  kqnrmlem1  20756  kqnrmlem2  20757  hmeoimaf1o  20783  reghmph  20806  nrmhmph  20807  filcon  20896  trfil1  20899  ufildr  20944  flimfil  20982  flimfnfcls  21041  alexsublem  21057  alexsubALTlem3  21062  ustbas2  21238  tgioo  21812  xrtgioo  21822  xrsmopn  21828  opnreen  21847  cnheibor  21981  cnllycmp  21982  lebnumlem1  21987  lebnumlem3  21989  lebnumlem1OLD  21990  lebnumlem3OLD  21992  bcthlem5  22294  bcth3  22297  voliunlem1  22501  voliunlem3  22503  volsup  22507  opnmbllem  22557  mbfimaopnlem  22609  lhop  22966  tglnpt  24592  tglineintmo  24685  ubthlem1  26510  shatomistici  28012  hatomistici  28013  unifi3  28295  tpr2rico  28726  hasheuni  28914  difelsiga  28963  prob01  29254  probdsb  29263  totprobd  29267  probmeasb  29271  cndprobtot  29277  orvcelval  29309  bnj1450  29867  bnj1501  29884  pconcon  29962  cvmsf1o  30003  cvmscld  30004  cvmsss2  30005  cvmopnlem  30009  cvmfolem  30010  cvmliftmolem1  30012  cvmliftlem6  30021  cvmliftlem8  30023  cvmlift2lem9  30042  cvmlift2lem11  30044  cvmlift2lem12  30045  cvmlift3lem6  30055  dfon2lem3  30438  dfon2lem7  30442  trpredpred  30476  frrlem11  30533  nobndlem2  30587  nobndlem8  30593  nofulllem3  30598  nofulllem5  30600  ntruni  30988  clsint2  30990  neibastop1  31020  topmeet  31025  topjoin  31026  fnemeet1  31027  fnejoin1  31029  opnmbllem0  31940  mbfresfi  31951  heiborlem1  32107  lssats  32547  dicval  34713  mapdunirnN  35187  isnacs3  35521  aomclem4  35885  kelac2  35893  stoweidlem28  37828  stoweidlem50  37851  stoweidlem52  37853  stoweidlem53  37854  stoweidlem54  37855  prsal  38100  salincl  38105  saliincl  38107  saldifcl2  38108  psmeasurelem  38216  caragenuni  38240  carageniuncl  38252  caratheodorylem1  38255  caratheodorylem2  38256