Theorem elssuni 4882

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  ∪ cuni 4851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852

This theorem is referenced by:  unissel  4883  ssunieq  4887  pwuni  4889  pwel  5318  uniopel  5464  dmrnssfld  5923  unixp0  6241  elfvunirn  6864  sorpssuni  7679  iunpw  7718  pwuninel2  8217  frrlem8  8236  frrlem10  8238  frrlem14  8242  fprresex  8253  onfununi  8274  tfrlem9  8317  tfrlem9a  8318  tfrlem13  8322  sbthlem1  9018  sbthlem2  9019  2pwuninel  9063  ordunifi  9193  unifpw  9258  fissuni  9260  unifi3  9265  dffi3  9337  cantnfp1lem3  9592  oemapvali  9596  cantnflem1  9601  cnfcom3lem  9615  rankuni2b  9768  carduni  9896  r0weon  9925  dfac8clem  9945  cardinfima  10010  alephfp  10021  iunfictbso  10027  dfac5lem4  10039  dfac5lem4OLD  10041  dfac2a  10043  dfacacn  10055  dfac12lem2  10058  kmlem2  10065  fin23lem16  10248  fin23lem21  10252  isf32lem5  10270  fin1a2lem11  10323  fin1a2lem13  10325  itunitc  10334  axdc2lem  10361  axdc3lem2  10364  ttukeylem5  10426  ttukeylem6  10427  fpwwe2lem10  10554  fpwwe2lem11  10555  fpwwe2lem12  10556  fpwwe2  10557  wunex2  10652  inatsk  10692  tskuni  10697  suplem1pr  10966  suplem2pr  10967  unirnioo  13393  mrcuni  17578  isacs3lem  18499  mrelatlub  18519  dprd2dlem1  20009  lbsextlem2  21149  eltopss  22882  toponss  22902  isbasis3g  22924  baspartn  22929  bastg  22941  tgcl  22944  fctop  22979  cctop  22981  ppttop  22982  epttop  22984  difopn  23009  ssntr  23033  isopn3  23041  isopn3i  23057  toponmre  23068  neiuni  23097  neiptoptop  23106  resttopon  23136  restopn2  23152  perfopn  23160  pnfnei  23195  mnfnei  23196  ssidcn  23230  lmcnp  23279  pnrmopn  23318  ist1-2  23322  nrmsep  23332  isnrm2  23333  isnrm3  23334  regsep2  23351  cncmp  23367  hauscmplem  23381  hauscmp  23382  conndisj  23391  cnconn  23397  conncompss  23408  islly2  23459  nllyrest  23461  nllyidm  23464  hausllycmp  23469  cldllycmp  23470  lly1stc  23471  comppfsc  23507  kgentopon  23513  kgenss  23518  llycmpkgen2  23525  1stckgen  23529  txuni2  23540  ptpjpre1  23546  ptuni2  23551  ptbasfi  23556  xkouni  23574  txcnpi  23583  ptpjopn  23587  txindis  23609  txnlly  23612  txtube  23615  hausdiag  23620  xkopt  23630  xkococnlem  23634  txconn  23664  qtopuni  23677  qtopkgen  23685  tgqtop  23687  regr1lem  23714  kqreglem1  23716  kqreglem2  23717  kqnrmlem1  23718  kqnrmlem2  23719  hmeoimaf1o  23745  reghmph  23768  nrmhmph  23769  filconn  23858  trfil1  23861  ufildr  23906  flimfil  23944  flimfnfcls  24003  alexsublem  24019  alexsubALTlem3  24024  ustbas2  24200  tgioo  24771  xrtgioo  24782  xrsmopn  24788  opnreen  24807  cnheibor  24932  cnllycmp  24933  lebnumlem1  24938  lebnumlem3  24940  bcthlem5  25305  bcth3  25308  voliunlem1  25527  voliunlem3  25529  volsup  25533  opnmbllem  25578  mbfimaopnlem  25632  lhop  25993  nosupno  27681  noinfno  27696  noetasuplem4  27714  noetainflem4  27718  tglnpt  28631  tglineintmo  28724  ubthlem1  30956  shatomistici  32447  hatomistici  32448  elrspunidl  33503  zarclsiin  34031  tpr2rico  34072  hasheuni  34245  difelsiga  34293  prob01  34573  probdsb  34582  totprobd  34586  probmeasb  34590  cndprobtot  34596  orvcelval  34629  bnj1450  35208  bnj1501  35225  elwf  35256  pconnconn  35429  cvmsf1o  35470  cvmscld  35471  cvmsss2  35472  cvmopnlem  35476  cvmfolem  35477  cvmliftmolem1  35479  cvmliftlem6  35488  cvmliftlem8  35490  cvmlift2lem9  35509  cvmlift2lem11  35511  cvmlift2lem12  35512  cvmlift3lem6  35522  dfon2lem3  35981  dfon2lem7  35985  ntruni  36525  clsint2  36527  neibastop1  36557  topmeet  36562  topjoin  36563  fnemeet1  36564  fnejoin1  36566  dfttc2g  36704  opnmbllem0  37991  mbfresfi  38001  heiborlem1  38146  lssats  39472  dicval  41636  mapdunirnN  42110  isnacs3  43156  aomclem4  43503  kelac2  43511  onsupuni  43675  onsupmaxb  43685  mnuunid  44722  mnutrcld  44724  grumnudlem  44730  wfac8prim  45447  ssuniint  45527  stoweidlem28  46474  stoweidlem50  46496  stoweidlem52  46498  stoweidlem53  46499  stoweidlem54  46500  prsal  46764  salincl  46770  saliinclf  46772  saldifcl2  46774  salexct  46780  psmeasurelem  46916  caragenuni  46957  carageniuncl  46969  caratheodorylem1  46972  caratheodorylem2  46973  voncmpl  47067  opncldeqv  49389  opndisj  49390  unilbeu  49472  setrec1lem2  50175  setrec2fun  50179