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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3898  ∪ cuni 4858

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-uni 4859

This theorem is referenced by:  unissel  4890  ssunieq  4894  pwuni  4896  pwel  5321  uniopel  5459  dmrnssfld  5917  unixp0  6235  elfvunirn  6858  sorpssuni  7671  iunpw  7710  pwuninel2  8210  frrlem8  8229  frrlem10  8231  frrlem14  8235  fprresex  8246  onfununi  8267  tfrlem9  8310  tfrlem9a  8311  tfrlem13  8315  sbthlem1  9007  sbthlem2  9008  2pwuninel  9052  ordunifi  9181  unifpw  9246  fissuni  9248  dffi3  9322  cantnfp1lem3  9577  oemapvali  9581  cantnflem1  9586  cnfcom3lem  9600  rankuni2b  9753  carduni  9881  r0weon  9910  dfac8clem  9930  cardinfima  9995  alephfp  10006  iunfictbso  10012  dfac5lem4  10024  dfac5lem4OLD  10026  dfac2a  10028  dfacacn  10040  dfac12lem2  10043  kmlem2  10050  fin23lem16  10233  fin23lem21  10237  isf32lem5  10255  fin1a2lem11  10308  fin1a2lem13  10310  itunitc  10319  axdc2lem  10346  axdc3lem2  10349  ttukeylem5  10411  ttukeylem6  10412  fpwwe2lem10  10538  fpwwe2lem11  10539  fpwwe2lem12  10540  fpwwe2  10541  wunex2  10636  inatsk  10676  tskuni  10681  suplem1pr  10950  suplem2pr  10951  unirnioo  13351  mrcuni  17529  isacs3lem  18450  mrelatlub  18470  dprd2dlem1  19957  lbsextlem2  21098  eltopss  22823  toponss  22843  isbasis3g  22865  baspartn  22870  bastg  22882  tgcl  22885  fctop  22920  cctop  22922  ppttop  22923  epttop  22925  difopn  22950  ssntr  22974  isopn3  22982  isopn3i  22998  toponmre  23009  neiuni  23038  neiptoptop  23047  resttopon  23077  restopn2  23093  perfopn  23101  pnfnei  23136  mnfnei  23137  ssidcn  23171  lmcnp  23220  pnrmopn  23259  ist1-2  23263  nrmsep  23273  isnrm2  23274  isnrm3  23275  regsep2  23292  cncmp  23308  hauscmplem  23322  hauscmp  23323  conndisj  23332  cnconn  23338  conncompss  23349  islly2  23400  nllyrest  23402  nllyidm  23405  hausllycmp  23410  cldllycmp  23411  lly1stc  23412  comppfsc  23448  kgentopon  23454  kgenss  23459  llycmpkgen2  23466  1stckgen  23470  txuni2  23481  ptpjpre1  23487  ptuni2  23492  ptbasfi  23497  xkouni  23515  txcnpi  23524  ptpjopn  23528  txindis  23550  txnlly  23553  txtube  23556  hausdiag  23561  xkopt  23571  xkococnlem  23575  txconn  23605  qtopuni  23618  qtopkgen  23626  tgqtop  23628  regr1lem  23655  kqreglem1  23657  kqreglem2  23658  kqnrmlem1  23659  kqnrmlem2  23660  hmeoimaf1o  23686  reghmph  23709  nrmhmph  23710  filconn  23799  trfil1  23802  ufildr  23847  flimfil  23885  flimfnfcls  23944  alexsublem  23960  alexsubALTlem3  23965  ustbas2  24141  tgioo  24712  xrtgioo  24723  xrsmopn  24729  opnreen  24748  cnheibor  24882  cnllycmp  24883  lebnumlem1  24888  lebnumlem3  24890  bcthlem5  25256  bcth3  25259  voliunlem1  25479  voliunlem3  25481  volsup  25485  opnmbllem  25530  mbfimaopnlem  25584  lhop  25949  nosupno  27643  noinfno  27658  noetasuplem4  27676  noetainflem4  27680  tglnpt  28528  tglineintmo  28621  ubthlem1  30852  shatomistici  32343  hatomistici  32344  unifi3  32698  elrspunidl  33400  zarclsiin  33905  tpr2rico  33946  hasheuni  34119  difelsiga  34167  prob01  34447  probdsb  34456  totprobd  34460  probmeasb  34464  cndprobtot  34470  orvcelval  34503  bnj1450  35083  bnj1501  35100  elwf  35129  pconnconn  35296  cvmsf1o  35337  cvmscld  35338  cvmsss2  35339  cvmopnlem  35343  cvmfolem  35344  cvmliftmolem1  35346  cvmliftlem6  35355  cvmliftlem8  35357  cvmlift2lem9  35376  cvmlift2lem11  35378  cvmlift2lem12  35379  cvmlift3lem6  35389  dfon2lem3  35848  dfon2lem7  35852  ntruni  36392  clsint2  36394  neibastop1  36424  topmeet  36429  topjoin  36430  fnemeet1  36431  fnejoin1  36433  opnmbllem0  37716  mbfresfi  37726  heiborlem1  37871  lssats  39131  dicval  41295  mapdunirnN  41769  isnacs3  42827  aomclem4  43174  kelac2  43182  onsupuni  43346  onsupmaxb  43356  mnuunid  44394  mnutrcld  44396  grumnudlem  44402  wfac8prim  45119  ssuniint  45199  stoweidlem28  46150  stoweidlem50  46172  stoweidlem52  46174  stoweidlem53  46175  stoweidlem54  46176  prsal  46440  salincl  46446  saliinclf  46448  saldifcl2  46450  salexct  46456  psmeasurelem  46592  caragenuni  46633  carageniuncl  46645  caratheodorylem1  46648  caratheodorylem2  46649  voncmpl  46743  opncldeqv  49026  opndisj  49027  unilbeu  49109  setrec1lem2  49813  setrec2fun  49817