Theorem elssuni 4900

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 3961	. 2 ⊢ 𝐴 ⊆ 𝐴
2		ssuni 4894	. 2 ⊢ ((𝐴 ⊆ 𝐴 ∧ 𝐴 ∈ 𝐵) → 𝐴 ⊆ ∪ 𝐵)
3	1, 2	mpan 702	1 ⊢ (𝐴 ∈ 𝐵 → 𝐴 ⊆ ∪ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2145   ⊆ wss 3907  ∪ cuni 4868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-uni 4869

This theorem is referenced by:  unissel  4901  ssunieq  4905  pwuni  4907  pwel  5343  uniopel  5490  dmrnssfld  5955  unixp0  6274  elfvunirn  6901  sorpssuni  7719  iunpw  7758  pwuninel2  8258  pwuninel  8259  frrlem8  8278  frrlem10  8280  frrlem14  8284  fprresex  8295  onfununi  8316  tfrlem9  8360  tfrlem9a  8361  tfrlem13  8365  sbthlem1  9063  sbthlem2  9064  2pwuninel  9108  ordunifi  9238  unifpw  9300  fissuni  9302  unifi3  9307  dffi3  9379  cantnfp1lem3  9637  oemapvali  9641  cantnflem1  9646  cnfcom3lem  9660  rankuni2b  9813  carduni  9955  r0weon  9984  dfac8clem  10004  cardinfima  10069  alephfp  10080  iunfictbso  10086  dfac5lem4  10098  dfac2a  10101  dfacacn  10113  dfac12lem2  10116  kmlem2  10123  fin23lem16  10307  fin23lem21  10311  isf32lem5  10329  fin1a2lem11  10382  fin1a2lem13  10384  itunitc  10393  axdc2lem  10420  axdc3lem2  10423  ttukeylem5  10485  ttukeylem6  10486  fpwwe2lem10  10613  fpwwe2lem11  10614  fpwwe2lem12  10615  fpwwe2  10616  wunex2  10711  inatsk  10751  tskuni  10756  suplem1pr  11025  suplem2pr  11026  unirnioo  13467  mrcuni  17667  isacs3lem  18588  mrelatlub  18608  dprd2dlem1  20104  lbsextlem2  21252  eltopss  23025  toponss  23045  isbasis3g  23067  baspartn  23072  bastg  23084  tgcl  23087  fctop  23122  cctop  23124  ppttop  23125  epttop  23127  difopn  23152  ssntr  23176  isopn3  23184  isopn3i  23200  toponmre  23211  neiuni  23240  neiptoptop  23249  resttopon  23279  restopn2  23295  perfopn  23303  pnfnei  23338  mnfnei  23339  ssidcn  23373  lmcnp  23422  pnrmopn  23461  ist1-2  23465  nrmsep  23475  isnrm2  23476  isnrm3  23477  regsep2  23494  cncmp  23510  hauscmplem  23524  hauscmp  23525  conndisj  23534  cnconn  23540  conncompss  23551  islly2  23602  nllyrest  23604  nllyidm  23607  hausllycmp  23612  cldllycmp  23613  lly1stc  23614  comppfsc  23650  kgentopon  23656  kgenss  23661  llycmpkgen2  23668  1stckgen  23672  txuni2  23683  ptpjpre1  23689  ptuni2  23694  ptbasfi  23699  xkouni  23717  txcnpi  23726  ptpjopn  23730  txindis  23752  txnlly  23755  txtube  23758  hausdiag  23763  xkopt  23773  xkococnlem  23777  txconn  23807  qtopuni  23820  qtopkgen  23828  tgqtop  23830  regr1lem  23857  kqreglem1  23859  kqreglem2  23860  kqnrmlem1  23861  kqnrmlem2  23862  hmeoimaf1o  23888  reghmph  23911  nrmhmph  23912  filconn  24001  trfil1  24004  ufildr  24049  flimfil  24087  flimfnfcls  24146  alexsublem  24162  alexsubALTlem3  24167  ustbas2  24343  tgioo  24914  xrtgioo  24925  xrsmopn  24931  opnreen  24950  cnheibor  25075  cnllycmp  25076  lebnumlem1  25081  lebnumlem3  25083  bcthlem5  25448  bcth3  25451  voliunlem1  25670  voliunlem3  25672  volsup  25676  opnmbllem  25721  mbfimaopnlem  25775  lhop  26136  nosupno  27825  noinfno  27840  noetasuplem4  27858  noetainflem4  27862  tglnpt  28776  tglineintmo  28869  ubthlem1  31131  shatomistici  32622  hatomistici  32623  elrspunidl  33652  zarclsiin  34178  tpr2rico  34219  hasheuni  34392  difelsiga  34440  prob01  34720  probdsb  34729  totprobd  34733  probmeasb  34737  cndprobtot  34743  orvcelval  34776  bnj1450  35355  bnj1501  35372  elwf  35405  pconnconn  35594  cvmsf1o  35635  cvmscld  35636  cvmsss2  35637  cvmopnlem  35641  cvmfolem  35642  cvmliftmolem1  35644  cvmliftlem6  35653  cvmliftlem8  35655  cvmlift2lem9  35674  cvmlift2lem11  35676  cvmlift2lem12  35677  cvmlift3lem6  35687  dfon2lem3  36146  dfon2lem7  36150  ntruni  36700  clsint2  36702  neibastop1  36732  topmeet  36737  topjoin  36738  fnemeet1  36739  fnejoin1  36741  dfttc2g  36879  opnmbllem0  38167  mbfresfi  38177  heiborlem1  38322  lssats  39648  dicval  41812  mapdunirnN  42286  isnacs3  43303  aomclem4  43646  kelac2  43654  onsupuni  43818  onsupmaxb  43828  mnuunid  44851  mnutrcld  44853  grumnudlem  44859  wfac8prim  45576  ssuniint  45656  stoweidlem28  46600  stoweidlem50  46622  stoweidlem52  46624  stoweidlem53  46625  stoweidlem54  46626  prsal  46890  salincl  46896  saliinclf  46898  saldifcl2  46900  salexct  46906  psmeasurelem  47042  caragenuni  47083  carageniuncl  47095  caratheodorylem1  47098  caratheodorylem2  47099  voncmpl  47193  opncldeqv  49531  opndisj  49532  unilbeu  49614  setrec1lem2  50317  setrec2fun  50321