Theorem elssuni 4889

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3902  ∪ cuni 4859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3919  df-uni 4860

This theorem is referenced by:  unissel  4890  ssunieq  4894  pwuni  4896  pwel  5319  uniopel  5456  dmrnssfld  5913  unixp0  6230  elfvunirn  6852  sorpssuni  7665  iunpw  7704  pwuninel2  8204  frrlem8  8223  frrlem10  8225  frrlem14  8229  fprresex  8240  onfununi  8261  tfrlem9  8304  tfrlem9a  8305  tfrlem13  8309  sbthlem1  9000  sbthlem2  9001  2pwuninel  9045  ordunifi  9174  unifpw  9239  fissuni  9241  dffi3  9315  cantnfp1lem3  9570  oemapvali  9574  cantnflem1  9579  cnfcom3lem  9593  rankuni2b  9743  carduni  9871  r0weon  9900  dfac8clem  9920  cardinfima  9985  alephfp  9996  iunfictbso  10002  dfac5lem4  10014  dfac5lem4OLD  10016  dfac2a  10018  dfacacn  10030  dfac12lem2  10033  kmlem2  10040  fin23lem16  10223  fin23lem21  10227  isf32lem5  10245  fin1a2lem11  10298  fin1a2lem13  10300  itunitc  10309  axdc2lem  10336  axdc3lem2  10339  ttukeylem5  10401  ttukeylem6  10402  fpwwe2lem10  10528  fpwwe2lem11  10529  fpwwe2lem12  10530  fpwwe2  10531  wunex2  10626  inatsk  10666  tskuni  10671  suplem1pr  10940  suplem2pr  10941  unirnioo  13346  mrcuni  17524  isacs3lem  18445  mrelatlub  18465  dprd2dlem1  19953  lbsextlem2  21094  eltopss  22820  toponss  22840  isbasis3g  22862  baspartn  22867  bastg  22879  tgcl  22882  fctop  22917  cctop  22919  ppttop  22920  epttop  22922  difopn  22947  ssntr  22971  isopn3  22979  isopn3i  22995  toponmre  23006  neiuni  23035  neiptoptop  23044  resttopon  23074  restopn2  23090  perfopn  23098  pnfnei  23133  mnfnei  23134  ssidcn  23168  lmcnp  23217  pnrmopn  23256  ist1-2  23260  nrmsep  23270  isnrm2  23271  isnrm3  23272  regsep2  23289  cncmp  23305  hauscmplem  23319  hauscmp  23320  conndisj  23329  cnconn  23335  conncompss  23346  islly2  23397  nllyrest  23399  nllyidm  23402  hausllycmp  23407  cldllycmp  23408  lly1stc  23409  comppfsc  23445  kgentopon  23451  kgenss  23456  llycmpkgen2  23463  1stckgen  23467  txuni2  23478  ptpjpre1  23484  ptuni2  23489  ptbasfi  23494  xkouni  23512  txcnpi  23521  ptpjopn  23525  txindis  23547  txnlly  23550  txtube  23553  hausdiag  23558  xkopt  23568  xkococnlem  23572  txconn  23602  qtopuni  23615  qtopkgen  23623  tgqtop  23625  regr1lem  23652  kqreglem1  23654  kqreglem2  23655  kqnrmlem1  23656  kqnrmlem2  23657  hmeoimaf1o  23683  reghmph  23706  nrmhmph  23707  filconn  23796  trfil1  23799  ufildr  23844  flimfil  23882  flimfnfcls  23941  alexsublem  23957  alexsubALTlem3  23962  ustbas2  24138  tgioo  24709  xrtgioo  24720  xrsmopn  24726  opnreen  24745  cnheibor  24879  cnllycmp  24880  lebnumlem1  24885  lebnumlem3  24887  bcthlem5  25253  bcth3  25256  voliunlem1  25476  voliunlem3  25478  volsup  25482  opnmbllem  25527  mbfimaopnlem  25581  lhop  25946  nosupno  27640  noinfno  27655  noetasuplem4  27673  noetainflem4  27677  tglnpt  28525  tglineintmo  28618  ubthlem1  30845  shatomistici  32336  hatomistici  32337  unifi3  32689  elrspunidl  33388  zarclsiin  33879  tpr2rico  33920  hasheuni  34093  difelsiga  34141  prob01  34421  probdsb  34430  totprobd  34434  probmeasb  34438  cndprobtot  34444  orvcelval  34477  bnj1450  35057  bnj1501  35074  elwf  35101  pconnconn  35263  cvmsf1o  35304  cvmscld  35305  cvmsss2  35306  cvmopnlem  35310  cvmfolem  35311  cvmliftmolem1  35313  cvmliftlem6  35322  cvmliftlem8  35324  cvmlift2lem9  35343  cvmlift2lem11  35345  cvmlift2lem12  35346  cvmlift3lem6  35356  dfon2lem3  35818  dfon2lem7  35822  ntruni  36360  clsint2  36362  neibastop1  36392  topmeet  36397  topjoin  36398  fnemeet1  36399  fnejoin1  36401  opnmbllem0  37695  mbfresfi  37705  heiborlem1  37850  lssats  39050  dicval  41214  mapdunirnN  41688  isnacs3  42742  aomclem4  43089  kelac2  43097  onsupuni  43261  onsupmaxb  43271  mnuunid  44309  mnutrcld  44311  grumnudlem  44317  wfac8prim  45034  ssuniint  45114  stoweidlem28  46065  stoweidlem50  46087  stoweidlem52  46089  stoweidlem53  46090  stoweidlem54  46091  prsal  46355  salincl  46361  saliinclf  46363  saldifcl2  46365  salexct  46371  psmeasurelem  46507  caragenuni  46548  carageniuncl  46560  caratheodorylem1  46563  caratheodorylem2  46564  voncmpl  46658  opncldeqv  48932  opndisj  48933  unilbeu  49015  setrec1lem2  49719  setrec2fun  49723