Theorem elssuni 4871

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	⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝐵)

Proof of Theorem elssuni

Step	Hyp	Ref	Expression
1		ssid 3943	. 2 ⊢ 𝐴 ⊆ 𝐴
2		ssuni 4866	. 2 ⊢ ((𝐴 ⊆ 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐴 ⊆ ∪ 𝐵)
3	1, 2	mpan 687	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3887  ∪ cuni 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840

This theorem is referenced by:  unissel  4872  ssunieq  4876  pwuni  4878  pwel  5304  uniopel  5430  dmrnssfld  5879  unixp0  6186  fvssunirn  6803  sorpssuni  7585  iunpw  7621  pwuninel2  8090  frrlem8  8109  frrlem10  8111  frrlem14  8115  fprresex  8126  wfrlem12OLD  8151  wfrlem16OLD  8155  wfrlem17OLD  8156  onfununi  8172  tfrlem9  8216  tfrlem9a  8217  tfrlem13  8221  sbthlem1  8870  sbthlem2  8871  2pwuninel  8919  ordunifi  9064  unifpw  9122  fissuni  9124  dffi3  9190  cantnfp1lem3  9438  oemapvali  9442  cantnflem1  9447  cnfcom3lem  9461  rankuni2b  9611  carduni  9739  r0weon  9768  dfac8clem  9788  cardinfima  9853  alephfp  9864  iunfictbso  9870  dfac5lem4  9882  dfac2a  9885  dfacacn  9897  dfac12lem2  9900  kmlem2  9907  fin23lem16  10091  fin23lem21  10095  isf32lem5  10113  fin1a2lem11  10166  fin1a2lem13  10168  itunitc  10177  axdc2lem  10204  axdc3lem2  10207  ttukeylem5  10269  ttukeylem6  10270  fpwwe2lem10  10396  fpwwe2lem11  10397  fpwwe2lem12  10398  fpwwe2  10399  wunex2  10494  inatsk  10534  tskuni  10539  suplem1pr  10808  suplem2pr  10809  unirnioo  13181  mrcuni  17330  isacs3lem  18260  mrelatlub  18280  dprd2dlem1  19644  lbsextlem2  20421  eltopss  22056  toponss  22076  isbasis3g  22099  baspartn  22104  bastg  22116  tgcl  22119  fctop  22154  cctop  22156  ppttop  22157  epttop  22159  difopn  22185  ssntr  22209  isopn3  22217  isopn3i  22233  toponmre  22244  neiuni  22273  neiptoptop  22282  resttopon  22312  restopn2  22328  perfopn  22336  pnfnei  22371  mnfnei  22372  ssidcn  22406  lmcnp  22455  pnrmopn  22494  ist1-2  22498  nrmsep  22508  isnrm2  22509  isnrm3  22510  regsep2  22527  cncmp  22543  hauscmplem  22557  hauscmp  22558  conndisj  22567  cnconn  22573  conncompss  22584  islly2  22635  nllyrest  22637  nllyidm  22640  hausllycmp  22645  cldllycmp  22646  lly1stc  22647  comppfsc  22683  kgentopon  22689  kgenss  22694  llycmpkgen2  22701  1stckgen  22705  txuni2  22716  ptpjpre1  22722  ptuni2  22727  ptbasfi  22732  xkouni  22750  txcnpi  22759  ptpjopn  22763  txindis  22785  txnlly  22788  txtube  22791  hausdiag  22796  xkopt  22806  xkococnlem  22810  txconn  22840  qtopuni  22853  qtopkgen  22861  tgqtop  22863  regr1lem  22890  kqreglem1  22892  kqreglem2  22893  kqnrmlem1  22894  kqnrmlem2  22895  hmeoimaf1o  22921  reghmph  22944  nrmhmph  22945  filconn  23034  trfil1  23037  ufildr  23082  flimfil  23120  flimfnfcls  23179  alexsublem  23195  alexsubALTlem3  23200  ustbas2  23377  tgioo  23959  xrtgioo  23969  xrsmopn  23975  opnreen  23994  cnheibor  24118  cnllycmp  24119  lebnumlem1  24124  lebnumlem3  24126  bcthlem5  24492  bcth3  24495  voliunlem1  24714  voliunlem3  24716  volsup  24720  opnmbllem  24765  mbfimaopnlem  24819  lhop  25180  tglnpt  26910  tglineintmo  27003  ubthlem1  29232  shatomistici  30723  hatomistici  30724  unifi3  31047  elrspunidl  31606  zarclsiin  31821  tpr2rico  31862  hasheuni  32053  difelsiga  32101  prob01  32380  probdsb  32389  totprobd  32393  probmeasb  32397  cndprobtot  32403  orvcelval  32435  bnj1450  33030  bnj1501  33047  pconnconn  33193  cvmsf1o  33234  cvmscld  33235  cvmsss2  33236  cvmopnlem  33240  cvmfolem  33241  cvmliftmolem1  33243  cvmliftlem6  33252  cvmliftlem8  33254  cvmlift2lem9  33273  cvmlift2lem11  33275  cvmlift2lem12  33276  cvmlift3lem6  33286  dfon2lem3  33761  dfon2lem7  33765  nosupno  33906  noinfno  33921  noetasuplem4  33939  noetainflem4  33943  ntruni  34516  clsint2  34518  neibastop1  34548  topmeet  34553  topjoin  34554  fnemeet1  34555  fnejoin1  34557  opnmbllem0  35813  mbfresfi  35823  heiborlem1  35969  lssats  37026  dicval  39190  mapdunirnN  39664  isnacs3  40532  aomclem4  40882  kelac2  40890  mnuunid  41895  mnutrcld  41897  grumnudlem  41903  ssuniint  42628  stoweidlem28  43569  stoweidlem50  43591  stoweidlem52  43593  stoweidlem53  43594  stoweidlem54  43595  prsal  43859  salincl  43864  saliincl  43866  saldifcl2  43867  salexct  43873  psmeasurelem  44008  caragenuni  44049  carageniuncl  44061  caratheodorylem1  44064  caratheodorylem2  44065  voncmpl  44159  opncldeqv  46195  opndisj  46196  unilbeu  46271  setrec1lem2  46394  setrec2fun  46398