Theorem elssuni 4109

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

Syntax hints:   -> wi 4   e. wcel 1755   C_ wss 3316   U.cuni 4079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-in 3323  df-ss 3330  df-uni 4080

This theorem is referenced by:  unissel  4110  ssunieq  4114  pwuni  4511  pwel  4532  uniopel  4583  dmrnssfld  5085  unixp0  5359  fvssunirn  5701  sorpssuni  6358  iunpw  6379  pwuninel2  6779  onfununi  6788  tfrlem9  6830  tfrlem9a  6831  tfrlem13  6835  sbthlem1  7409  sbthlem2  7410  2pwuninel  7454  ordunifi  7550  unifpw  7602  fissuni  7604  dffi3  7669  cantnfp1lem3  7876  oemapvali  7880  cantnflem1  7885  cantnfp1lem3OLD  7902  cantnflem1OLD  7908  cnfcom3lem  7924  cnfcom3lemOLD  7932  rankuni2b  8048  carduni  8139  r0weon  8167  dfac8clem  8190  cardinfima  8255  alephfp  8266  iunfictbso  8272  dfac5lem4  8284  dfac2a  8287  dfacacn  8298  dfac12lem2  8301  kmlem2  8308  fin23lem16  8492  fin23lem21  8496  isf32lem5  8514  fin1a2lem11  8567  fin1a2lem13  8569  itunitc  8578  axdc2lem  8605  axdc3lem2  8608  ttukeylem5  8670  ttukeylem6  8671  fpwwe2lem11  8795  fpwwe2lem12  8796  fpwwe2lem13  8797  fpwwe2  8798  wunex2  8893  inatsk  8933  tskuni  8938  suplem1pr  9209  suplem2pr  9210  unirnioo  11377  mrcuni  14542  isacs3lem  15319  mrelatlub  15339  dprd2dlem1  16514  lbsextlem2  17162  eltopss  18362  toponss  18376  isbasis3g  18396  baspartn  18401  bastg  18413  tgcl  18416  fctop  18450  cctop  18452  ppttop  18453  epttop  18455  difopn  18480  ssntr  18504  isopn3  18512  isopn3i  18528  toponmre  18539  neiuni  18568  neiptoptop  18577  resttopon  18607  restopn2  18623  perfopn  18631  pnfnei  18666  mnfnei  18667  ssidcn  18701  lmcnp  18750  pnrmopn  18789  ist1-2  18793  nrmsep  18803  isnrm2  18804  isnrm3  18805  regsep2  18822  cncmp  18837  hauscmplem  18851  hauscmp  18852  conndisj  18862  cnconn  18868  concompss  18879  islly2  18930  nllyrest  18932  nllyidm  18935  hausllycmp  18940  cldllycmp  18941  lly1stc  18942  kgentopon  18953  kgenss  18958  llycmpkgen2  18965  1stckgen  18969  txuni2  18980  ptpjpre1  18986  ptuni2  18991  ptbasfi  18996  xkouni  19014  txcnpi  19023  ptpjopn  19027  txindis  19049  txnlly  19052  txtube  19055  hausdiag  19060  xkopt  19070  xkococnlem  19074  txcon  19104  qtopuni  19117  qtopkgen  19125  tgqtop  19127  regr1lem  19154  kqreglem1  19156  kqreglem2  19157  kqnrmlem1  19158  kqnrmlem2  19159  hmeoimaf1o  19185  reghmph  19208  nrmhmph  19209  filcon  19298  trfil1  19301  ufildr  19346  flimfil  19384  flimfnfcls  19443  alexsublem  19458  alexsubALTlem3  19463  ustbas2  19642  tgioo  20215  xrtgioo  20225  xrsmopn  20231  opnreen  20250  cnheibor  20369  cnllycmp  20370  lebnumlem1  20375  lebnumlem3  20377  bcthlem5  20681  bcth3  20684  voliunlem1  20873  voliunlem3  20875  volsup  20879  opnmbllem  20923  mbfimaopnlem  20975  lhop  21330  tglineintmo  22917  ubthlem1  24094  shatomistici  25588  hatomistici  25589  unifi3  25829  tpr2rico  26196  hasheuni  26388  difelsiga  26430  prob01  26644  probdsb  26653  totprobd  26657  probmeasb  26661  cndprobtot  26667  orvcelval  26699  pconcon  26968  cvmsf1o  27009  cvmscld  27010  cvmsss2  27011  cvmopnlem  27015  cvmfolem  27016  cvmliftmolem1  27018  cvmliftlem6  27027  cvmliftlem8  27029  cvmlift2lem9  27048  cvmlift2lem11  27050  cvmlift2lem12  27051  cvmlift3lem6  27061  dfon2lem3  27445  dfon2lem7  27449  trpredpred  27539  wfrlem12  27582  wfrlem16  27586  frrlem11  27627  nobndlem2  27681  nobndlem8  27687  nofulllem3  27692  nofulllem5  27694  opnmbllem0  28271  mbfresfi  28282  ntruni  28366  clsint2  28368  comppfsc  28423  neibastop1  28424  topmeet  28429  topjoin  28430  fnemeet1  28431  fnejoin1  28433  heiborlem1  28554  isnacs3  28891  aomclem4  29255  kelac2  29263  stoweidlem28  29669  stoweidlem50  29691  stoweidlem52  29693  stoweidlem53  29694  stoweidlem54  29695  bnj1450  31743  bnj1501  31760  lssats  32230  dicval  34394  mapdunirnN  34868