Theorem elssuni 4219

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 3473	. 2 |- A C_ A
2		ssuni 4211	. 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 1758   C_ wss 3426   U.cuni 4189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3070  df-in 3433  df-ss 3440  df-uni 4190

This theorem is referenced by:  unissel  4220  ssunieq  4224  pwuni  4621  pwel  4642  uniopel  4693  dmrnssfld  5196  unixp0  5469  fvssunirn  5812  sorpssuni  6469  iunpw  6490  pwuninel2  6893  onfununi  6902  tfrlem9  6944  tfrlem9a  6945  tfrlem13  6949  sbthlem1  7521  sbthlem2  7522  2pwuninel  7566  ordunifi  7663  unifpw  7715  fissuni  7717  dffi3  7782  cantnfp1lem3  7989  oemapvali  7993  cantnflem1  7998  cantnfp1lem3OLD  8015  cantnflem1OLD  8021  cnfcom3lem  8037  cnfcom3lemOLD  8045  rankuni2b  8161  carduni  8252  r0weon  8280  dfac8clem  8303  cardinfima  8368  alephfp  8379  iunfictbso  8385  dfac5lem4  8397  dfac2a  8400  dfacacn  8411  dfac12lem2  8414  kmlem2  8421  fin23lem16  8605  fin23lem21  8609  isf32lem5  8627  fin1a2lem11  8680  fin1a2lem13  8682  itunitc  8691  axdc2lem  8718  axdc3lem2  8721  ttukeylem5  8783  ttukeylem6  8784  fpwwe2lem11  8908  fpwwe2lem12  8909  fpwwe2lem13  8910  fpwwe2  8911  wunex2  9006  inatsk  9046  tskuni  9051  suplem1pr  9322  suplem2pr  9323  unirnioo  11490  mrcuni  14661  isacs3lem  15438  mrelatlub  15458  dprd2dlem1  16645  lbsextlem2  17346  eltopss  18636  toponss  18650  isbasis3g  18670  baspartn  18675  bastg  18687  tgcl  18690  fctop  18724  cctop  18726  ppttop  18727  epttop  18729  difopn  18754  ssntr  18778  isopn3  18786  isopn3i  18802  toponmre  18813  neiuni  18842  neiptoptop  18851  resttopon  18881  restopn2  18897  perfopn  18905  pnfnei  18940  mnfnei  18941  ssidcn  18975  lmcnp  19024  pnrmopn  19063  ist1-2  19067  nrmsep  19077  isnrm2  19078  isnrm3  19079  regsep2  19096  cncmp  19111  hauscmplem  19125  hauscmp  19126  conndisj  19136  cnconn  19142  concompss  19153  islly2  19204  nllyrest  19206  nllyidm  19209  hausllycmp  19214  cldllycmp  19215  lly1stc  19216  kgentopon  19227  kgenss  19232  llycmpkgen2  19239  1stckgen  19243  txuni2  19254  ptpjpre1  19260  ptuni2  19265  ptbasfi  19270  xkouni  19288  txcnpi  19297  ptpjopn  19301  txindis  19323  txnlly  19326  txtube  19329  hausdiag  19334  xkopt  19344  xkococnlem  19348  txcon  19378  qtopuni  19391  qtopkgen  19399  tgqtop  19401  regr1lem  19428  kqreglem1  19430  kqreglem2  19431  kqnrmlem1  19432  kqnrmlem2  19433  hmeoimaf1o  19459  reghmph  19482  nrmhmph  19483  filcon  19572  trfil1  19575  ufildr  19620  flimfil  19658  flimfnfcls  19717  alexsublem  19732  alexsubALTlem3  19737  ustbas2  19916  tgioo  20489  xrtgioo  20499  xrsmopn  20505  opnreen  20524  cnheibor  20643  cnllycmp  20644  lebnumlem1  20649  lebnumlem3  20651  bcthlem5  20955  bcth3  20958  voliunlem1  21147  voliunlem3  21149  volsup  21153  opnmbllem  21197  mbfimaopnlem  21249  lhop  21604  tglnpt  23102  tglineintmo  23169  ubthlem1  24406  shatomistici  25900  hatomistici  25901  unifi3  26139  tpr2rico  26476  hasheuni  26668  difelsiga  26710  prob01  26930  probdsb  26939  totprobd  26943  probmeasb  26947  cndprobtot  26953  orvcelval  26985  pconcon  27254  cvmsf1o  27295  cvmscld  27296  cvmsss2  27297  cvmopnlem  27301  cvmfolem  27302  cvmliftmolem1  27304  cvmliftlem6  27313  cvmliftlem8  27315  cvmlift2lem9  27334  cvmlift2lem11  27336  cvmlift2lem12  27337  cvmlift3lem6  27347  dfon2lem3  27732  dfon2lem7  27736  trpredpred  27826  wfrlem12  27869  wfrlem16  27873  frrlem11  27914  nobndlem2  27968  nobndlem8  27974  nofulllem3  27979  nofulllem5  27981  opnmbllem0  28565  mbfresfi  28576  ntruni  28660  clsint2  28662  comppfsc  28717  neibastop1  28718  topmeet  28723  topjoin  28724  fnemeet1  28725  fnejoin1  28727  heiborlem1  28848  isnacs3  29184  aomclem4  29548  kelac2  29556  stoweidlem28  29961  stoweidlem50  29983  stoweidlem52  29985  stoweidlem53  29986  stoweidlem54  29987  bnj1450  32341  bnj1501  32358  lssats  32963  dicval  35127  mapdunirnN  35601