Theorem elssuni 4264

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 3508	. 2 |- A C_ A
2		ssuni 4256	. 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 1804   C_ wss 3461   U.cuni 4234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468  df-ss 3475  df-uni 4235

This theorem is referenced by:  unissel  4265  ssunieq  4269  pwuni  4668  pwel  4689  uniopel  4741  dmrnssfld  5251  unixp0  5531  fvssunirn  5879  sorpssuni  6574  iunpw  6599  pwuninel2  7005  onfununi  7014  tfrlem9  7056  tfrlem9a  7057  tfrlem13  7061  sbthlem1  7629  sbthlem2  7630  2pwuninel  7674  ordunifi  7772  unifpw  7825  fissuni  7827  dffi3  7893  cantnfp1lem3  8102  oemapvali  8106  cantnflem1  8111  cantnfp1lem3OLD  8128  cantnflem1OLD  8134  cnfcom3lem  8150  cnfcom3lemOLD  8158  rankuni2b  8274  carduni  8365  r0weon  8393  dfac8clem  8416  cardinfima  8481  alephfp  8492  iunfictbso  8498  dfac5lem4  8510  dfac2a  8513  dfacacn  8524  dfac12lem2  8527  kmlem2  8534  fin23lem16  8718  fin23lem21  8722  isf32lem5  8740  fin1a2lem11  8793  fin1a2lem13  8795  itunitc  8804  axdc2lem  8831  axdc3lem2  8834  ttukeylem5  8896  ttukeylem6  8897  fpwwe2lem11  9021  fpwwe2lem12  9022  fpwwe2lem13  9023  fpwwe2  9024  wunex2  9119  inatsk  9159  tskuni  9164  suplem1pr  9433  suplem2pr  9434  unirnioo  11633  mrcuni  14895  isacs3lem  15670  mrelatlub  15690  dprd2dlem1  16964  lbsextlem2  17679  eltopss  19289  toponss  19303  isbasis3g  19323  baspartn  19328  bastg  19340  tgcl  19344  fctop  19378  cctop  19380  ppttop  19381  epttop  19383  difopn  19408  ssntr  19432  isopn3  19440  isopn3i  19456  toponmre  19467  neiuni  19496  neiptoptop  19505  resttopon  19535  restopn2  19551  perfopn  19559  pnfnei  19594  mnfnei  19595  ssidcn  19629  lmcnp  19678  pnrmopn  19717  ist1-2  19721  nrmsep  19731  isnrm2  19732  isnrm3  19733  regsep2  19750  cncmp  19765  hauscmplem  19779  hauscmp  19780  conndisj  19790  cnconn  19796  concompss  19807  islly2  19858  nllyrest  19860  nllyidm  19863  hausllycmp  19868  cldllycmp  19869  lly1stc  19870  comppfsc  19906  kgentopon  19912  kgenss  19917  llycmpkgen2  19924  1stckgen  19928  txuni2  19939  ptpjpre1  19945  ptuni2  19950  ptbasfi  19955  xkouni  19973  txcnpi  19982  ptpjopn  19986  txindis  20008  txnlly  20011  txtube  20014  hausdiag  20019  xkopt  20029  xkococnlem  20033  txcon  20063  qtopuni  20076  qtopkgen  20084  tgqtop  20086  regr1lem  20113  kqreglem1  20115  kqreglem2  20116  kqnrmlem1  20117  kqnrmlem2  20118  hmeoimaf1o  20144  reghmph  20167  nrmhmph  20168  filcon  20257  trfil1  20260  ufildr  20305  flimfil  20343  flimfnfcls  20402  alexsublem  20417  alexsubALTlem3  20422  ustbas2  20601  tgioo  21174  xrtgioo  21184  xrsmopn  21190  opnreen  21209  cnheibor  21328  cnllycmp  21329  lebnumlem1  21334  lebnumlem3  21336  bcthlem5  21640  bcth3  21643  voliunlem1  21833  voliunlem3  21835  volsup  21839  opnmbllem  21883  mbfimaopnlem  21935  lhop  22290  tglnpt  23808  tglineintmo  23894  ubthlem1  25658  shatomistici  27152  hatomistici  27153  unifi3  27400  tpr2rico  27767  hasheuni  27964  difelsiga  28006  prob01  28225  probdsb  28234  totprobd  28238  probmeasb  28242  cndprobtot  28248  orvcelval  28280  pconcon  28549  cvmsf1o  28590  cvmscld  28591  cvmsss2  28592  cvmopnlem  28596  cvmfolem  28597  cvmliftmolem1  28599  cvmliftlem6  28608  cvmliftlem8  28610  cvmlift2lem9  28629  cvmlift2lem11  28631  cvmlift2lem12  28632  cvmlift3lem6  28642  dfon2lem3  29192  dfon2lem7  29196  trpredpred  29286  wfrlem12  29329  wfrlem16  29333  frrlem11  29374  nobndlem2  29428  nobndlem8  29434  nofulllem3  29439  nofulllem5  29441  opnmbllem0  30025  mbfresfi  30036  ntruni  30120  clsint2  30122  neibastop1  30152  topmeet  30157  topjoin  30158  fnemeet1  30159  fnejoin1  30161  heiborlem1  30282  isnacs3  30617  aomclem4  30978  kelac2  30986  stoweidlem28  31699  stoweidlem50  31721  stoweidlem52  31723  stoweidlem53  31724  stoweidlem54  31725  bnj1450  33839  bnj1501  33856  lssats  34477  dicval  36643  mapdunirnN  37117