Theorem elssuni 4891

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3905  ∪ cuni 4861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-uni 4862

This theorem is referenced by:  unissel  4892  ssunieq  4896  pwuni  4898  pwel  5323  uniopel  5463  dmrnssfld  5919  unixp0  6235  elfvunirn  6856  fvssunirnOLD  6858  sorpssuni  7672  iunpw  7711  pwuninel2  8214  frrlem8  8233  frrlem10  8235  frrlem14  8239  fprresex  8250  onfununi  8271  tfrlem9  8314  tfrlem9a  8315  tfrlem13  8319  sbthlem1  9011  sbthlem2  9012  2pwuninel  9056  ordunifi  9195  unifpw  9264  fissuni  9266  dffi3  9340  cantnfp1lem3  9595  oemapvali  9599  cantnflem1  9604  cnfcom3lem  9618  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  10553  fpwwe2lem11  10554  fpwwe2lem12  10555  fpwwe2  10556  wunex2  10651  inatsk  10691  tskuni  10696  suplem1pr  10965  suplem2pr  10966  unirnioo  13370  mrcuni  17545  isacs3lem  18466  mrelatlub  18486  dprd2dlem1  19940  lbsextlem2  21084  eltopss  22810  toponss  22830  isbasis3g  22852  baspartn  22857  bastg  22869  tgcl  22872  fctop  22907  cctop  22909  ppttop  22910  epttop  22912  difopn  22937  ssntr  22961  isopn3  22969  isopn3i  22985  toponmre  22996  neiuni  23025  neiptoptop  23034  resttopon  23064  restopn2  23080  perfopn  23088  pnfnei  23123  mnfnei  23124  ssidcn  23158  lmcnp  23207  pnrmopn  23246  ist1-2  23250  nrmsep  23260  isnrm2  23261  isnrm3  23262  regsep2  23279  cncmp  23295  hauscmplem  23309  hauscmp  23310  conndisj  23319  cnconn  23325  conncompss  23336  islly2  23387  nllyrest  23389  nllyidm  23392  hausllycmp  23397  cldllycmp  23398  lly1stc  23399  comppfsc  23435  kgentopon  23441  kgenss  23446  llycmpkgen2  23453  1stckgen  23457  txuni2  23468  ptpjpre1  23474  ptuni2  23479  ptbasfi  23484  xkouni  23502  txcnpi  23511  ptpjopn  23515  txindis  23537  txnlly  23540  txtube  23543  hausdiag  23548  xkopt  23558  xkococnlem  23562  txconn  23592  qtopuni  23605  qtopkgen  23613  tgqtop  23615  regr1lem  23642  kqreglem1  23644  kqreglem2  23645  kqnrmlem1  23646  kqnrmlem2  23647  hmeoimaf1o  23673  reghmph  23696  nrmhmph  23697  filconn  23786  trfil1  23789  ufildr  23834  flimfil  23872  flimfnfcls  23931  alexsublem  23947  alexsubALTlem3  23952  ustbas2  24129  tgioo  24700  xrtgioo  24711  xrsmopn  24717  opnreen  24736  cnheibor  24870  cnllycmp  24871  lebnumlem1  24876  lebnumlem3  24878  bcthlem5  25244  bcth3  25247  voliunlem1  25467  voliunlem3  25469  volsup  25473  opnmbllem  25518  mbfimaopnlem  25572  lhop  25937  nosupno  27631  noinfno  27646  noetasuplem4  27664  noetainflem4  27668  tglnpt  28512  tglineintmo  28605  ubthlem1  30832  shatomistici  32323  hatomistici  32324  unifi3  32669  elrspunidl  33375  zarclsiin  33837  tpr2rico  33878  hasheuni  34051  difelsiga  34099  prob01  34380  probdsb  34389  totprobd  34393  probmeasb  34397  cndprobtot  34403  orvcelval  34436  bnj1450  35016  bnj1501  35033  pconnconn  35203  cvmsf1o  35244  cvmscld  35245  cvmsss2  35246  cvmopnlem  35250  cvmfolem  35251  cvmliftmolem1  35253  cvmliftlem6  35262  cvmliftlem8  35264  cvmlift2lem9  35283  cvmlift2lem11  35285  cvmlift2lem12  35286  cvmlift3lem6  35296  dfon2lem3  35758  dfon2lem7  35762  ntruni  36300  clsint2  36302  neibastop1  36332  topmeet  36337  topjoin  36338  fnemeet1  36339  fnejoin1  36341  opnmbllem0  37635  mbfresfi  37645  heiborlem1  37790  lssats  38990  dicval  41155  mapdunirnN  41629  isnacs3  42683  aomclem4  43030  kelac2  43038  onsupuni  43202  onsupmaxb  43212  mnuunid  44250  mnutrcld  44252  grumnudlem  44258  wfac8prim  44976  ssuniint  45056  stoweidlem28  46010  stoweidlem50  46032  stoweidlem52  46034  stoweidlem53  46035  stoweidlem54  46036  prsal  46300  salincl  46306  saliinclf  46308  saldifcl2  46310  salexct  46316  psmeasurelem  46452  caragenuni  46493  carageniuncl  46505  caratheodorylem1  46508  caratheodorylem2  46509  voncmpl  46603  opncldeqv  48887  opndisj  48888  unilbeu  48970  setrec1lem2  49674  setrec2fun  49678