Theorem elssuni 4116

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

Syntax hints:   -> wi 4   e. wcel 1756   C_ wss 3323   U.cuni 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-ss 3337  df-uni 4087

This theorem is referenced by:  unissel  4117  ssunieq  4121  pwuni  4518  pwel  4539  uniopel  4590  dmrnssfld  5093  unixp0  5366  fvssunirn  5708  sorpssuni  6364  iunpw  6385  pwuninel2  6785  onfununi  6794  tfrlem9  6836  tfrlem9a  6837  tfrlem13  6841  sbthlem1  7413  sbthlem2  7414  2pwuninel  7458  ordunifi  7554  unifpw  7606  fissuni  7608  dffi3  7673  cantnfp1lem3  7880  oemapvali  7884  cantnflem1  7889  cantnfp1lem3OLD  7906  cantnflem1OLD  7912  cnfcom3lem  7928  cnfcom3lemOLD  7936  rankuni2b  8052  carduni  8143  r0weon  8171  dfac8clem  8194  cardinfima  8259  alephfp  8270  iunfictbso  8276  dfac5lem4  8288  dfac2a  8291  dfacacn  8302  dfac12lem2  8305  kmlem2  8312  fin23lem16  8496  fin23lem21  8500  isf32lem5  8518  fin1a2lem11  8571  fin1a2lem13  8573  itunitc  8582  axdc2lem  8609  axdc3lem2  8612  ttukeylem5  8674  ttukeylem6  8675  fpwwe2lem11  8799  fpwwe2lem12  8800  fpwwe2lem13  8801  fpwwe2  8802  wunex2  8897  inatsk  8937  tskuni  8942  suplem1pr  9213  suplem2pr  9214  unirnioo  11381  mrcuni  14551  isacs3lem  15328  mrelatlub  15348  dprd2dlem1  16530  lbsextlem2  17220  eltopss  18500  toponss  18514  isbasis3g  18534  baspartn  18539  bastg  18551  tgcl  18554  fctop  18588  cctop  18590  ppttop  18591  epttop  18593  difopn  18618  ssntr  18642  isopn3  18650  isopn3i  18666  toponmre  18677  neiuni  18706  neiptoptop  18715  resttopon  18745  restopn2  18761  perfopn  18769  pnfnei  18804  mnfnei  18805  ssidcn  18839  lmcnp  18888  pnrmopn  18927  ist1-2  18931  nrmsep  18941  isnrm2  18942  isnrm3  18943  regsep2  18960  cncmp  18975  hauscmplem  18989  hauscmp  18990  conndisj  19000  cnconn  19006  concompss  19017  islly2  19068  nllyrest  19070  nllyidm  19073  hausllycmp  19078  cldllycmp  19079  lly1stc  19080  kgentopon  19091  kgenss  19096  llycmpkgen2  19103  1stckgen  19107  txuni2  19118  ptpjpre1  19124  ptuni2  19129  ptbasfi  19134  xkouni  19152  txcnpi  19161  ptpjopn  19165  txindis  19187  txnlly  19190  txtube  19193  hausdiag  19198  xkopt  19208  xkococnlem  19212  txcon  19242  qtopuni  19255  qtopkgen  19263  tgqtop  19265  regr1lem  19292  kqreglem1  19294  kqreglem2  19295  kqnrmlem1  19296  kqnrmlem2  19297  hmeoimaf1o  19323  reghmph  19346  nrmhmph  19347  filcon  19436  trfil1  19439  ufildr  19484  flimfil  19522  flimfnfcls  19581  alexsublem  19596  alexsubALTlem3  19601  ustbas2  19780  tgioo  20353  xrtgioo  20363  xrsmopn  20369  opnreen  20388  cnheibor  20507  cnllycmp  20508  lebnumlem1  20513  lebnumlem3  20515  bcthlem5  20819  bcth3  20822  voliunlem1  21011  voliunlem3  21013  volsup  21017  opnmbllem  21061  mbfimaopnlem  21113  lhop  21468  tglnpt  22963  tglineintmo  23027  ubthlem1  24239  shatomistici  25733  hatomistici  25734  unifi3  25973  tpr2rico  26311  hasheuni  26503  difelsiga  26545  prob01  26765  probdsb  26774  totprobd  26778  probmeasb  26782  cndprobtot  26788  orvcelval  26820  pconcon  27089  cvmsf1o  27130  cvmscld  27131  cvmsss2  27132  cvmopnlem  27136  cvmfolem  27137  cvmliftmolem1  27139  cvmliftlem6  27148  cvmliftlem8  27150  cvmlift2lem9  27169  cvmlift2lem11  27171  cvmlift2lem12  27172  cvmlift3lem6  27182  dfon2lem3  27567  dfon2lem7  27571  trpredpred  27661  wfrlem12  27704  wfrlem16  27708  frrlem11  27749  nobndlem2  27803  nobndlem8  27809  nofulllem3  27814  nofulllem5  27816  opnmbllem0  28398  mbfresfi  28409  ntruni  28493  clsint2  28495  comppfsc  28550  neibastop1  28551  topmeet  28556  topjoin  28557  fnemeet1  28558  fnejoin1  28560  heiborlem1  28681  isnacs3  29017  aomclem4  29381  kelac2  29389  stoweidlem28  29794  stoweidlem50  29816  stoweidlem52  29818  stoweidlem53  29819  stoweidlem54  29820  bnj1450  31970  bnj1501  31987  lssats  32550  dicval  34714  mapdunirnN  35188