Theorem elssuni 4877

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

Syntax hints:   → wi 4   ∈ wcel 2110   ⊆ wss 3892  ∪ cuni 4845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909  df-uni 4846

This theorem is referenced by:  unissel  4878  ssunieq  4882  pwuni  4884  pwel  5308  uniopel  5433  dmrnssfld  5877  unixp0  6184  fvssunirn  6798  sorpssuni  7577  iunpw  7613  pwuninel2  8079  frrlem8  8098  frrlem10  8100  frrlem14  8104  fprresex  8115  wfrlem12OLD  8140  wfrlem16OLD  8144  wfrlem17OLD  8145  onfununi  8161  tfrlem9  8205  tfrlem9a  8206  tfrlem13  8210  sbthlem1  8850  sbthlem2  8851  2pwuninel  8899  ordunifi  9040  unifpw  9098  fissuni  9100  dffi3  9166  cantnfp1lem3  9414  oemapvali  9418  cantnflem1  9423  cnfcom3lem  9437  trpredpred  9473  rankuni2b  9610  carduni  9738  r0weon  9767  dfac8clem  9787  cardinfima  9852  alephfp  9863  iunfictbso  9869  dfac5lem4  9881  dfac2a  9884  dfacacn  9896  dfac12lem2  9899  kmlem2  9906  fin23lem16  10090  fin23lem21  10094  isf32lem5  10112  fin1a2lem11  10165  fin1a2lem13  10167  itunitc  10176  axdc2lem  10203  axdc3lem2  10206  ttukeylem5  10268  ttukeylem6  10269  fpwwe2lem10  10395  fpwwe2lem11  10396  fpwwe2lem12  10397  fpwwe2  10398  wunex2  10493  inatsk  10533  tskuni  10538  suplem1pr  10807  suplem2pr  10808  unirnioo  13178  mrcuni  17326  isacs3lem  18256  mrelatlub  18276  dprd2dlem1  19640  lbsextlem2  20417  eltopss  22052  toponss  22072  isbasis3g  22095  baspartn  22100  bastg  22112  tgcl  22115  fctop  22150  cctop  22152  ppttop  22153  epttop  22155  difopn  22181  ssntr  22205  isopn3  22213  isopn3i  22229  toponmre  22240  neiuni  22269  neiptoptop  22278  resttopon  22308  restopn2  22324  perfopn  22332  pnfnei  22367  mnfnei  22368  ssidcn  22402  lmcnp  22451  pnrmopn  22490  ist1-2  22494  nrmsep  22504  isnrm2  22505  isnrm3  22506  regsep2  22523  cncmp  22539  hauscmplem  22553  hauscmp  22554  conndisj  22563  cnconn  22569  conncompss  22580  islly2  22631  nllyrest  22633  nllyidm  22636  hausllycmp  22641  cldllycmp  22642  lly1stc  22643  comppfsc  22679  kgentopon  22685  kgenss  22690  llycmpkgen2  22697  1stckgen  22701  txuni2  22712  ptpjpre1  22718  ptuni2  22723  ptbasfi  22728  xkouni  22746  txcnpi  22755  ptpjopn  22759  txindis  22781  txnlly  22784  txtube  22787  hausdiag  22792  xkopt  22802  xkococnlem  22806  txconn  22836  qtopuni  22849  qtopkgen  22857  tgqtop  22859  regr1lem  22886  kqreglem1  22888  kqreglem2  22889  kqnrmlem1  22890  kqnrmlem2  22891  hmeoimaf1o  22917  reghmph  22940  nrmhmph  22941  filconn  23030  trfil1  23033  ufildr  23078  flimfil  23116  flimfnfcls  23175  alexsublem  23191  alexsubALTlem3  23196  ustbas2  23373  tgioo  23955  xrtgioo  23965  xrsmopn  23971  opnreen  23990  cnheibor  24114  cnllycmp  24115  lebnumlem1  24120  lebnumlem3  24122  bcthlem5  24488  bcth3  24491  voliunlem1  24710  voliunlem3  24712  volsup  24716  opnmbllem  24761  mbfimaopnlem  24815  lhop  25176  tglnpt  26906  tglineintmo  26999  ubthlem1  29226  shatomistici  30717  hatomistici  30718  unifi3  31041  elrspunidl  31600  zarclsiin  31815  tpr2rico  31856  hasheuni  32047  difelsiga  32095  prob01  32374  probdsb  32383  totprobd  32387  probmeasb  32391  cndprobtot  32397  orvcelval  32429  bnj1450  33024  bnj1501  33041  pconnconn  33187  cvmsf1o  33228  cvmscld  33229  cvmsss2  33230  cvmopnlem  33234  cvmfolem  33235  cvmliftmolem1  33237  cvmliftlem6  33246  cvmliftlem8  33248  cvmlift2lem9  33267  cvmlift2lem11  33269  cvmlift2lem12  33270  cvmlift3lem6  33280  dfon2lem3  33755  dfon2lem7  33759  nosupno  33900  noinfno  33915  noetasuplem4  33933  noetainflem4  33937  ntruni  34510  clsint2  34512  neibastop1  34542  topmeet  34547  topjoin  34548  fnemeet1  34549  fnejoin1  34551  opnmbllem0  35807  mbfresfi  35817  heiborlem1  35963  lssats  37020  dicval  39184  mapdunirnN  39658  isnacs3  40527  aomclem4  40877  kelac2  40885  mnuunid  41863  mnutrcld  41865  grumnudlem  41871  ssuniint  42596  stoweidlem28  43538  stoweidlem50  43560  stoweidlem52  43562  stoweidlem53  43563  stoweidlem54  43564  prsal  43828  salincl  43833  saliincl  43835  saldifcl2  43836  salexct  43842  psmeasurelem  43977  caragenuni  44018  carageniuncl  44030  caratheodorylem1  44033  caratheodorylem2  44034  voncmpl  44128  opncldeqv  46162  opndisj  46163  unilbeu  46238  setrec1lem2  46361  setrec2fun  46365