Theorem elssuni 4904

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3917  ∪ cuni 4874

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-uni 4875

This theorem is referenced by:  unissel  4905  ssunieq  4910  pwuni  4912  pwel  5339  uniopel  5479  dmrnssfld  5940  unixp0  6259  elfvunirn  6893  fvssunirnOLD  6895  sorpssuni  7711  iunpw  7750  pwuninel2  8256  frrlem8  8275  frrlem10  8277  frrlem14  8281  fprresex  8292  onfununi  8313  tfrlem9  8356  tfrlem9a  8357  tfrlem13  8361  sbthlem1  9057  sbthlem2  9058  2pwuninel  9102  ordunifi  9244  unifpw  9313  fissuni  9315  dffi3  9389  cantnfp1lem3  9640  oemapvali  9644  cantnflem1  9649  cnfcom3lem  9663  rankuni2b  9813  carduni  9941  r0weon  9972  dfac8clem  9992  cardinfima  10057  alephfp  10068  iunfictbso  10074  dfac5lem4  10086  dfac5lem4OLD  10088  dfac2a  10090  dfacacn  10102  dfac12lem2  10105  kmlem2  10112  fin23lem16  10295  fin23lem21  10299  isf32lem5  10317  fin1a2lem11  10370  fin1a2lem13  10372  itunitc  10381  axdc2lem  10408  axdc3lem2  10411  ttukeylem5  10473  ttukeylem6  10474  fpwwe2lem10  10600  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  wunex2  10698  inatsk  10738  tskuni  10743  suplem1pr  11012  suplem2pr  11013  unirnioo  13417  mrcuni  17589  isacs3lem  18508  mrelatlub  18528  dprd2dlem1  19980  lbsextlem2  21076  eltopss  22801  toponss  22821  isbasis3g  22843  baspartn  22848  bastg  22860  tgcl  22863  fctop  22898  cctop  22900  ppttop  22901  epttop  22903  difopn  22928  ssntr  22952  isopn3  22960  isopn3i  22976  toponmre  22987  neiuni  23016  neiptoptop  23025  resttopon  23055  restopn2  23071  perfopn  23079  pnfnei  23114  mnfnei  23115  ssidcn  23149  lmcnp  23198  pnrmopn  23237  ist1-2  23241  nrmsep  23251  isnrm2  23252  isnrm3  23253  regsep2  23270  cncmp  23286  hauscmplem  23300  hauscmp  23301  conndisj  23310  cnconn  23316  conncompss  23327  islly2  23378  nllyrest  23380  nllyidm  23383  hausllycmp  23388  cldllycmp  23389  lly1stc  23390  comppfsc  23426  kgentopon  23432  kgenss  23437  llycmpkgen2  23444  1stckgen  23448  txuni2  23459  ptpjpre1  23465  ptuni2  23470  ptbasfi  23475  xkouni  23493  txcnpi  23502  ptpjopn  23506  txindis  23528  txnlly  23531  txtube  23534  hausdiag  23539  xkopt  23549  xkococnlem  23553  txconn  23583  qtopuni  23596  qtopkgen  23604  tgqtop  23606  regr1lem  23633  kqreglem1  23635  kqreglem2  23636  kqnrmlem1  23637  kqnrmlem2  23638  hmeoimaf1o  23664  reghmph  23687  nrmhmph  23688  filconn  23777  trfil1  23780  ufildr  23825  flimfil  23863  flimfnfcls  23922  alexsublem  23938  alexsubALTlem3  23943  ustbas2  24120  tgioo  24691  xrtgioo  24702  xrsmopn  24708  opnreen  24727  cnheibor  24861  cnllycmp  24862  lebnumlem1  24867  lebnumlem3  24869  bcthlem5  25235  bcth3  25238  voliunlem1  25458  voliunlem3  25460  volsup  25464  opnmbllem  25509  mbfimaopnlem  25563  lhop  25928  nosupno  27622  noinfno  27637  noetasuplem4  27655  noetainflem4  27659  tglnpt  28483  tglineintmo  28576  ubthlem1  30806  shatomistici  32297  hatomistici  32298  unifi3  32643  elrspunidl  33406  zarclsiin  33868  tpr2rico  33909  hasheuni  34082  difelsiga  34130  prob01  34411  probdsb  34420  totprobd  34424  probmeasb  34428  cndprobtot  34434  orvcelval  34467  bnj1450  35047  bnj1501  35064  pconnconn  35225  cvmsf1o  35266  cvmscld  35267  cvmsss2  35268  cvmopnlem  35272  cvmfolem  35273  cvmliftmolem1  35275  cvmliftlem6  35284  cvmliftlem8  35286  cvmlift2lem9  35305  cvmlift2lem11  35307  cvmlift2lem12  35308  cvmlift3lem6  35318  dfon2lem3  35780  dfon2lem7  35784  ntruni  36322  clsint2  36324  neibastop1  36354  topmeet  36359  topjoin  36360  fnemeet1  36361  fnejoin1  36363  opnmbllem0  37657  mbfresfi  37667  heiborlem1  37812  lssats  39012  dicval  41177  mapdunirnN  41651  isnacs3  42705  aomclem4  43053  kelac2  43061  onsupuni  43225  onsupmaxb  43235  mnuunid  44273  mnutrcld  44275  grumnudlem  44281  wfac8prim  44999  ssuniint  45079  stoweidlem28  46033  stoweidlem50  46055  stoweidlem52  46057  stoweidlem53  46058  stoweidlem54  46059  prsal  46323  salincl  46329  saliinclf  46331  saldifcl2  46333  salexct  46339  psmeasurelem  46475  caragenuni  46516  carageniuncl  46528  caratheodorylem1  46531  caratheodorylem2  46532  voncmpl  46626  opncldeqv  48894  opndisj  48895  unilbeu  48977  setrec1lem2  49681  setrec2fun  49685