Theorem elssuni 4268

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 3516	. 2 |- A C_ A
2		ssuni 4260	. 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 1762   C_ wss 3469   U.cuni 4238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-v 3108  df-in 3476  df-ss 3483  df-uni 4239

This theorem is referenced by:  unissel  4269  ssunieq  4273  pwuni  4671  pwel  4692  uniopel  4744  dmrnssfld  5252  unixp0  5532  fvssunirn  5880  sorpssuni  6564  iunpw  6585  pwuninel2  6993  onfununi  7002  tfrlem9  7044  tfrlem9a  7045  tfrlem13  7049  sbthlem1  7617  sbthlem2  7618  2pwuninel  7662  ordunifi  7759  unifpw  7812  fissuni  7814  dffi3  7880  cantnfp1lem3  8088  oemapvali  8092  cantnflem1  8097  cantnfp1lem3OLD  8114  cantnflem1OLD  8120  cnfcom3lem  8136  cnfcom3lemOLD  8144  rankuni2b  8260  carduni  8351  r0weon  8379  dfac8clem  8402  cardinfima  8467  alephfp  8478  iunfictbso  8484  dfac5lem4  8496  dfac2a  8499  dfacacn  8510  dfac12lem2  8513  kmlem2  8520  fin23lem16  8704  fin23lem21  8708  isf32lem5  8726  fin1a2lem11  8779  fin1a2lem13  8781  itunitc  8790  axdc2lem  8817  axdc3lem2  8820  ttukeylem5  8882  ttukeylem6  8883  fpwwe2lem11  9007  fpwwe2lem12  9008  fpwwe2lem13  9009  fpwwe2  9010  wunex2  9105  inatsk  9145  tskuni  9150  suplem1pr  9419  suplem2pr  9420  unirnioo  11613  mrcuni  14865  isacs3lem  15642  mrelatlub  15662  dprd2dlem1  16873  lbsextlem2  17581  eltopss  19176  toponss  19190  isbasis3g  19210  baspartn  19215  bastg  19227  tgcl  19230  fctop  19264  cctop  19266  ppttop  19267  epttop  19269  difopn  19294  ssntr  19318  isopn3  19326  isopn3i  19342  toponmre  19353  neiuni  19382  neiptoptop  19391  resttopon  19421  restopn2  19437  perfopn  19445  pnfnei  19480  mnfnei  19481  ssidcn  19515  lmcnp  19564  pnrmopn  19603  ist1-2  19607  nrmsep  19617  isnrm2  19618  isnrm3  19619  regsep2  19636  cncmp  19651  hauscmplem  19665  hauscmp  19666  conndisj  19676  cnconn  19682  concompss  19693  islly2  19744  nllyrest  19746  nllyidm  19749  hausllycmp  19754  cldllycmp  19755  lly1stc  19756  kgentopon  19767  kgenss  19772  llycmpkgen2  19779  1stckgen  19783  txuni2  19794  ptpjpre1  19800  ptuni2  19805  ptbasfi  19810  xkouni  19828  txcnpi  19837  ptpjopn  19841  txindis  19863  txnlly  19866  txtube  19869  hausdiag  19874  xkopt  19884  xkococnlem  19888  txcon  19918  qtopuni  19931  qtopkgen  19939  tgqtop  19941  regr1lem  19968  kqreglem1  19970  kqreglem2  19971  kqnrmlem1  19972  kqnrmlem2  19973  hmeoimaf1o  19999  reghmph  20022  nrmhmph  20023  filcon  20112  trfil1  20115  ufildr  20160  flimfil  20198  flimfnfcls  20257  alexsublem  20272  alexsubALTlem3  20277  ustbas2  20456  tgioo  21029  xrtgioo  21039  xrsmopn  21045  opnreen  21064  cnheibor  21183  cnllycmp  21184  lebnumlem1  21189  lebnumlem3  21191  bcthlem5  21495  bcth3  21498  voliunlem1  21688  voliunlem3  21690  volsup  21694  opnmbllem  21738  mbfimaopnlem  21790  lhop  22145  tglnpt  23657  tglineintmo  23728  ubthlem1  25312  shatomistici  26806  hatomistici  26807  unifi3  27050  tpr2rico  27380  hasheuni  27581  difelsiga  27623  prob01  27842  probdsb  27851  totprobd  27855  probmeasb  27859  cndprobtot  27865  orvcelval  27897  pconcon  28166  cvmsf1o  28207  cvmscld  28208  cvmsss2  28209  cvmopnlem  28213  cvmfolem  28214  cvmliftmolem1  28216  cvmliftlem6  28225  cvmliftlem8  28227  cvmlift2lem9  28246  cvmlift2lem11  28248  cvmlift2lem12  28249  cvmlift3lem6  28259  dfon2lem3  28644  dfon2lem7  28648  trpredpred  28738  wfrlem12  28781  wfrlem16  28785  frrlem11  28826  nobndlem2  28880  nobndlem8  28886  nofulllem3  28891  nofulllem5  28893  opnmbllem0  29478  mbfresfi  29489  ntruni  29573  clsint2  29575  comppfsc  29630  neibastop1  29631  topmeet  29636  topjoin  29637  fnemeet1  29638  fnejoin1  29640  heiborlem1  29761  isnacs3  30097  aomclem4  30460  kelac2  30468  stoweidlem28  31147  stoweidlem50  31169  stoweidlem52  31171  stoweidlem53  31172  stoweidlem54  31173  bnj1450  33060  bnj1501  33077  lssats  33684  dicval  35848  mapdunirnN  36322