Theorem elssuni 4868

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3883  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837

This theorem is referenced by:  unissel  4869  ssunieq  4873  pwuni  4875  pwel  5299  uniopel  5424  dmrnssfld  5868  unixp0  6175  fvssunirn  6785  sorpssuni  7563  iunpw  7599  pwuninel2  8061  frrlem8  8080  frrlem10  8082  frrlem14  8086  fprresex  8097  wfrlem12OLD  8122  wfrlem16OLD  8126  wfrlem17OLD  8127  onfununi  8143  tfrlem9  8187  tfrlem9a  8188  tfrlem13  8192  sbthlem1  8823  sbthlem2  8824  2pwuninel  8868  ordunifi  8994  unifpw  9052  fissuni  9054  dffi3  9120  cantnfp1lem3  9368  oemapvali  9372  cantnflem1  9377  cnfcom3lem  9391  trpredpred  9406  rankuni2b  9542  carduni  9670  r0weon  9699  dfac8clem  9719  cardinfima  9784  alephfp  9795  iunfictbso  9801  dfac5lem4  9813  dfac2a  9816  dfacacn  9828  dfac12lem2  9831  kmlem2  9838  fin23lem16  10022  fin23lem21  10026  isf32lem5  10044  fin1a2lem11  10097  fin1a2lem13  10099  itunitc  10108  axdc2lem  10135  axdc3lem2  10138  ttukeylem5  10200  ttukeylem6  10201  fpwwe2lem10  10327  fpwwe2lem11  10328  fpwwe2lem12  10329  fpwwe2  10330  wunex2  10425  inatsk  10465  tskuni  10470  suplem1pr  10739  suplem2pr  10740  unirnioo  13110  mrcuni  17247  isacs3lem  18175  mrelatlub  18195  dprd2dlem1  19559  lbsextlem2  20336  eltopss  21964  toponss  21984  isbasis3g  22007  baspartn  22012  bastg  22024  tgcl  22027  fctop  22062  cctop  22064  ppttop  22065  epttop  22067  difopn  22093  ssntr  22117  isopn3  22125  isopn3i  22141  toponmre  22152  neiuni  22181  neiptoptop  22190  resttopon  22220  restopn2  22236  perfopn  22244  pnfnei  22279  mnfnei  22280  ssidcn  22314  lmcnp  22363  pnrmopn  22402  ist1-2  22406  nrmsep  22416  isnrm2  22417  isnrm3  22418  regsep2  22435  cncmp  22451  hauscmplem  22465  hauscmp  22466  conndisj  22475  cnconn  22481  conncompss  22492  islly2  22543  nllyrest  22545  nllyidm  22548  hausllycmp  22553  cldllycmp  22554  lly1stc  22555  comppfsc  22591  kgentopon  22597  kgenss  22602  llycmpkgen2  22609  1stckgen  22613  txuni2  22624  ptpjpre1  22630  ptuni2  22635  ptbasfi  22640  xkouni  22658  txcnpi  22667  ptpjopn  22671  txindis  22693  txnlly  22696  txtube  22699  hausdiag  22704  xkopt  22714  xkococnlem  22718  txconn  22748  qtopuni  22761  qtopkgen  22769  tgqtop  22771  regr1lem  22798  kqreglem1  22800  kqreglem2  22801  kqnrmlem1  22802  kqnrmlem2  22803  hmeoimaf1o  22829  reghmph  22852  nrmhmph  22853  filconn  22942  trfil1  22945  ufildr  22990  flimfil  23028  flimfnfcls  23087  alexsublem  23103  alexsubALTlem3  23108  ustbas2  23285  tgioo  23865  xrtgioo  23875  xrsmopn  23881  opnreen  23900  cnheibor  24024  cnllycmp  24025  lebnumlem1  24030  lebnumlem3  24032  bcthlem5  24397  bcth3  24400  voliunlem1  24619  voliunlem3  24621  volsup  24625  opnmbllem  24670  mbfimaopnlem  24724  lhop  25085  tglnpt  26814  tglineintmo  26907  ubthlem1  29133  shatomistici  30624  hatomistici  30625  unifi3  30949  elrspunidl  31508  zarclsiin  31723  tpr2rico  31764  hasheuni  31953  difelsiga  32001  prob01  32280  probdsb  32289  totprobd  32293  probmeasb  32297  cndprobtot  32303  orvcelval  32335  bnj1450  32930  bnj1501  32947  pconnconn  33093  cvmsf1o  33134  cvmscld  33135  cvmsss2  33136  cvmopnlem  33140  cvmfolem  33141  cvmliftmolem1  33143  cvmliftlem6  33152  cvmliftlem8  33154  cvmlift2lem9  33173  cvmlift2lem11  33175  cvmlift2lem12  33176  cvmlift3lem6  33186  dfon2lem3  33667  dfon2lem7  33671  nosupno  33833  noinfno  33848  noetasuplem4  33866  noetainflem4  33870  ntruni  34443  clsint2  34445  neibastop1  34475  topmeet  34480  topjoin  34481  fnemeet1  34482  fnejoin1  34484  opnmbllem0  35740  mbfresfi  35750  heiborlem1  35896  lssats  36953  dicval  39117  mapdunirnN  39591  isnacs3  40448  aomclem4  40798  kelac2  40806  mnuunid  41784  mnutrcld  41786  grumnudlem  41792  ssuniint  42517  stoweidlem28  43459  stoweidlem50  43481  stoweidlem52  43483  stoweidlem53  43484  stoweidlem54  43485  prsal  43749  salincl  43754  saliincl  43756  saldifcl2  43757  salexct  43763  psmeasurelem  43898  caragenuni  43939  carageniuncl  43951  caratheodorylem1  43954  caratheodorylem2  43955  voncmpl  44049  opncldeqv  46083  opndisj  46084  unilbeu  46159  setrec1lem2  46280  setrec2fun  46284