Theorem elssuni 4902

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3902  ∪ cuni 4870

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871

This theorem is used by:  unissel  4903  ssunieq  4907  pwuni  4909  pwel  5350  uniopel  5497  dmrnssfld  5962  unixp0  6285  elfvunirn  6912  sorpssuni  7737  iunpw  7774  pwuninel2  8276  pwuninel  8277  frrlem8  8296  frrlem10  8298  frrlem14  8302  fprresex  8313  onfununi  8334  tfrlem9  8378  tfrlem9a  8379  tfrlem13  8383  sbthlem1  9089  sbthlem2  9090  2pwuninel  9134  ordunifi  9264  unifpw  9326  fissuni  9328  unifi3  9333  dffi3  9405  cantnfp1lem3  9663  oemapvali  9667  cantnflem1  9672  cnfcom3lem  9686  rankuni2b  9839  carduni  9990  r0weon  10019  dfac8clem  10039  cardinfima  10104  alephfp  10115  iunfictbso  10121  dfac5lem4  10133  dfac2a  10136  dfacacn  10148  dfac12lem2  10151  kmlem2  10158  fin23lem16  10341  fin23lem21  10345  isf32lem5  10363  fin1a2lem11  10416  fin1a2lem13  10418  itunitc  10427  axdc2lem  10454  axdc3lem2  10457  ttukeylem5  10519  ttukeylem6  10520  fpwwe2lem10  10653  fpwwe2lem11  10654  fpwwe2lem12  10655  fpwwe2  10656  wunex2  10751  inatsk  10791  tskuni  10796  suplem1pr  11065  suplem2pr  11066  unirnioo  13506  mrcuni  17715  isacs3lem  18636  mrelatlub  18656  dprd2dlem1  20176  lbsextlem2  21352  eltopss  23138  toponss  23158  isbasis3g  23180  baspartn  23185  bastg  23197  tgcl  23200  fctop  23235  cctop  23237  ppttop  23238  epttop  23240  difopn  23265  ssntr  23289  isopn3  23297  isopn3i  23313  toponmre  23324  neiuni  23353  neiptoptop  23362  resttopon  23392  restopn2  23408  perfopn  23416  pnfnei  23451  mnfnei  23452  ssidcn  23486  lmcnp  23535  pnrmopn  23574  ist1-2  23578  nrmsep  23588  isnrm2  23589  isnrm3  23590  regsep2  23607  cncmp  23623  hauscmplem  23637  hauscmp  23638  conndisj  23647  cnconn  23653  conncompss  23664  islly2  23716  nllyrest  23718  nllyidm  23721  hausllycmp  23726  cldllycmp  23727  lly1stc  23728  comppfsc  23764  kgentopon  23770  kgenss  23775  llycmpkgen2  23782  1stckgen  23786  txuni2  23797  ptpjpre1  23803  ptuni2  23808  ptbasfi  23813  xkouni  23831  txcnpi  23840  ptpjopn  23844  txindis  23866  txnlly  23869  txtube  23872  hausdiag  23877  xkopt  23887  xkococnlem  23891  txconn  23921  qtopuni  23934  qtopkgen  23942  tgqtop  23944  regr1lem  23971  kqreglem1  23973  kqreglem2  23974  kqnrmlem1  23975  kqnrmlem2  23976  hmeoimaf1o  24002  reghmph  24025  nrmhmph  24026  filconn  24115  trfil1  24118  ufildr  24163  flimfil  24201  flimfnfcls  24260  alexsublem  24276  alexsubALTlem3  24281  ustbas2  24457  tgioo  25028  xrtgioo  25039  xrsmopn  25045  opnreen  25064  cnheibor  25189  cnllycmp  25190  lebnumlem1  25195  lebnumlem3  25197  bcthlem5  25562  bcth3  25565  voliunlem1  25784  voliunlem3  25786  volsup  25790  opnmbllem  25835  mbfimaopnlem  25889  lhop  26250  nosupno  27947  noinfno  27962  noetasuplem4  27980  noetainflem4  27984  tglnpt  28899  tglineintmo  28997  ubthlem1  31359  shatomistici  32850  hatomistici  32851  elrspunidl  33864  zarclsiin  34389  tpr2rico  34430  hasheuni  34603  prob01  34932  probdsb  34941  totprobd  34945  probmeasb  34949  cndprobtot  34955  orvcelval  34988  bnj1450  35567  bnj1501  35584  elwf  35612  pconnconn  35818  cvmsf1o  35859  cvmscld  35860  cvmsss2  35861  cvmopnlem  35865  cvmfolem  35866  cvmliftmolem1  35868  cvmliftlem6  35877  cvmliftlem8  35879  cvmlift2lem9  35898  cvmlift2lem11  35900  cvmlift2lem12  35901  cvmlift3lem6  35911  dfon2lem3  36370  dfon2lem7  36374  ntruni  36954  clsint2  36956  neibastop1  36986  topmeet  36991  topjoin  36992  fnemeet1  36993  fnejoin1  36995  dfttc2g  37133  opnmbllem0  38413  mbfresfi  38423  heiborlem1  38569  lssats  39893  dicval  42057  mapdunirnN  42531  isnacs3  43563  aomclem4  43906  kelac2  43914  onsupuni  44078  onsupmaxb  44088  mnuunid  45109  mnutrcld  45111  grumnudlem  45117  wfac8prim  45833  ssuniint  45920  stoweidlem28  46864  stoweidlem50  46886  stoweidlem52  46888  stoweidlem53  46889  stoweidlem54  46890  prsal  47154  salincl  47160  saliinclf  47162  saldifcl2  47164  salexct  47170  psmeasurelem  47306  caragenuni  47347  carageniuncl  47359  caratheodorylem1  47362  caratheodorylem2  47363  voncmpl  47457  opncldeqv  49836  opndisj  49837  unilbeu  49919  setrec1lem2  50622  setrec2fun  50626