Theorem elssuni 4896

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

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3904  ∪ cuni 4864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-uni 4865

This theorem is referenced by:  unissel  4897  ssunieq  4901  pwuni  4903  pwel  5337  uniopel  5484  dmrnssfld  5948  unixp0  6266  elfvunirn  6893  sorpssuni  7711  iunpw  7750  pwuninel2  8249  pwuninel  8250  frrlem8  8269  frrlem10  8271  frrlem14  8275  fprresex  8286  onfununi  8307  tfrlem9  8351  tfrlem9a  8352  tfrlem13  8356  sbthlem1  9055  sbthlem2  9056  2pwuninel  9100  ordunifi  9230  unifpw  9295  fissuni  9297  unifi3  9302  dffi3  9374  cantnfp1lem3  9632  oemapvali  9636  cantnflem1  9641  cnfcom3lem  9655  rankuni2b  9808  carduni  9936  r0weon  9965  dfac8clem  9985  cardinfima  10050  alephfp  10061  iunfictbso  10067  dfac5lem4  10079  dfac5lem4OLD  10081  dfac2a  10083  dfacacn  10095  dfac12lem2  10098  kmlem2  10105  fin23lem16  10289  fin23lem21  10293  isf32lem5  10311  fin1a2lem11  10364  fin1a2lem13  10366  itunitc  10375  axdc2lem  10402  axdc3lem2  10405  ttukeylem5  10467  ttukeylem6  10468  fpwwe2lem10  10595  fpwwe2lem11  10596  fpwwe2lem12  10597  fpwwe2  10598  wunex2  10693  inatsk  10733  tskuni  10738  suplem1pr  11007  suplem2pr  11008  unirnioo  13450  mrcuni  17636  isacs3lem  18557  mrelatlub  18577  dprd2dlem1  20066  lbsextlem2  21209  eltopss  22947  toponss  22967  isbasis3g  22989  baspartn  22994  bastg  23006  tgcl  23009  fctop  23044  cctop  23046  ppttop  23047  epttop  23049  difopn  23074  ssntr  23098  isopn3  23106  isopn3i  23122  toponmre  23133  neiuni  23162  neiptoptop  23171  resttopon  23201  restopn2  23217  perfopn  23225  pnfnei  23260  mnfnei  23261  ssidcn  23295  lmcnp  23344  pnrmopn  23383  ist1-2  23387  nrmsep  23397  isnrm2  23398  isnrm3  23399  regsep2  23416  cncmp  23432  hauscmplem  23446  hauscmp  23447  conndisj  23456  cnconn  23462  conncompss  23473  islly2  23524  nllyrest  23526  nllyidm  23529  hausllycmp  23534  cldllycmp  23535  lly1stc  23536  comppfsc  23572  kgentopon  23578  kgenss  23583  llycmpkgen2  23590  1stckgen  23594  txuni2  23605  ptpjpre1  23611  ptuni2  23616  ptbasfi  23621  xkouni  23639  txcnpi  23648  ptpjopn  23652  txindis  23674  txnlly  23677  txtube  23680  hausdiag  23685  xkopt  23695  xkococnlem  23699  txconn  23729  qtopuni  23742  qtopkgen  23750  tgqtop  23752  regr1lem  23779  kqreglem1  23781  kqreglem2  23782  kqnrmlem1  23783  kqnrmlem2  23784  hmeoimaf1o  23810  reghmph  23833  nrmhmph  23834  filconn  23923  trfil1  23926  ufildr  23971  flimfil  24009  flimfnfcls  24068  alexsublem  24084  alexsubALTlem3  24089  ustbas2  24265  tgioo  24836  xrtgioo  24847  xrsmopn  24853  opnreen  24872  cnheibor  24997  cnllycmp  24998  lebnumlem1  25003  lebnumlem3  25005  bcthlem5  25370  bcth3  25373  voliunlem1  25592  voliunlem3  25594  volsup  25598  opnmbllem  25643  mbfimaopnlem  25697  lhop  26058  nosupno  27744  noinfno  27759  noetasuplem4  27777  noetainflem4  27781  tglnpt  28695  tglineintmo  28788  ubthlem1  31019  shatomistici  32510  hatomistici  32511  elrspunidl  33575  zarclsiin  34129  tpr2rico  34170  hasheuni  34343  difelsiga  34391  prob01  34671  probdsb  34680  totprobd  34684  probmeasb  34688  cndprobtot  34694  orvcelval  34727  bnj1450  35309  bnj1501  35326  elwf  35357  pconnconn  35545  cvmsf1o  35586  cvmscld  35587  cvmsss2  35588  cvmopnlem  35592  cvmfolem  35593  cvmliftmolem1  35595  cvmliftlem6  35604  cvmliftlem8  35606  cvmlift2lem9  35625  cvmlift2lem11  35627  cvmlift2lem12  35628  cvmlift3lem6  35638  dfon2lem3  36097  dfon2lem7  36101  ntruni  36651  clsint2  36653  neibastop1  36683  topmeet  36688  topjoin  36689  fnemeet1  36690  fnejoin1  36692  dfttc2g  36830  opnmbllem0  38119  mbfresfi  38129  heiborlem1  38274  lssats  39600  dicval  41764  mapdunirnN  42238  isnacs3  43255  aomclem4  43598  kelac2  43606  onsupuni  43770  onsupmaxb  43780  mnuunid  44817  mnutrcld  44819  grumnudlem  44825  wfac8prim  45542  ssuniint  45622  stoweidlem28  46566  stoweidlem50  46588  stoweidlem52  46590  stoweidlem53  46591  stoweidlem54  46592  prsal  46856  salincl  46862  saliinclf  46864  saldifcl2  46866  salexct  46872  psmeasurelem  47008  caragenuni  47049  carageniuncl  47061  caratheodorylem1  47064  caratheodorylem2  47065  voncmpl  47159  opncldeqv  49487  opndisj  49488  unilbeu  49570  setrec1lem2  50273  setrec2fun  50277