Theorem elssuni 4876

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

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3890  ∪ 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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-uni 4846

This theorem is referenced by:  unissel  4877  ssunieq  4881  pwuni  4883  pwel  5317  uniopel  5464  dmrnssfld  5923  unixp0  6241  elfvunirn  6864  sorpssuni  7682  iunpw  7721  pwuninel2  8221  frrlem8  8240  frrlem10  8242  frrlem14  8246  fprresex  8257  onfununi  8278  tfrlem9  8321  tfrlem9a  8322  tfrlem13  8326  sbthlem1  9022  sbthlem2  9023  2pwuninel  9067  ordunifi  9197  unifpw  9262  fissuni  9264  unifi3  9269  dffi3  9341  cantnfp1lem3  9599  oemapvali  9603  cantnflem1  9608  cnfcom3lem  9622  rankuni2b  9775  carduni  9903  r0weon  9932  dfac8clem  9952  cardinfima  10017  alephfp  10028  iunfictbso  10034  dfac5lem4  10046  dfac5lem4OLD  10048  dfac2a  10050  dfacacn  10062  dfac12lem2  10065  kmlem2  10072  fin23lem16  10255  fin23lem21  10259  isf32lem5  10277  fin1a2lem11  10330  fin1a2lem13  10332  itunitc  10341  axdc2lem  10368  axdc3lem2  10371  ttukeylem5  10433  ttukeylem6  10434  fpwwe2lem10  10561  fpwwe2lem11  10562  fpwwe2lem12  10563  fpwwe2  10564  wunex2  10659  inatsk  10699  tskuni  10704  suplem1pr  10973  suplem2pr  10974  unirnioo  13400  mrcuni  17585  isacs3lem  18506  mrelatlub  18526  dprd2dlem1  20016  lbsextlem2  21159  eltopss  22897  toponss  22917  isbasis3g  22939  baspartn  22944  bastg  22956  tgcl  22959  fctop  22994  cctop  22996  ppttop  22997  epttop  22999  difopn  23024  ssntr  23048  isopn3  23056  isopn3i  23072  toponmre  23083  neiuni  23112  neiptoptop  23121  resttopon  23151  restopn2  23167  perfopn  23175  pnfnei  23210  mnfnei  23211  ssidcn  23245  lmcnp  23294  pnrmopn  23333  ist1-2  23337  nrmsep  23347  isnrm2  23348  isnrm3  23349  regsep2  23366  cncmp  23382  hauscmplem  23396  hauscmp  23397  conndisj  23406  cnconn  23412  conncompss  23423  islly2  23474  nllyrest  23476  nllyidm  23479  hausllycmp  23484  cldllycmp  23485  lly1stc  23486  comppfsc  23522  kgentopon  23528  kgenss  23533  llycmpkgen2  23540  1stckgen  23544  txuni2  23555  ptpjpre1  23561  ptuni2  23566  ptbasfi  23571  xkouni  23589  txcnpi  23598  ptpjopn  23602  txindis  23624  txnlly  23627  txtube  23630  hausdiag  23635  xkopt  23645  xkococnlem  23649  txconn  23679  qtopuni  23692  qtopkgen  23700  tgqtop  23702  regr1lem  23729  kqreglem1  23731  kqreglem2  23732  kqnrmlem1  23733  kqnrmlem2  23734  hmeoimaf1o  23760  reghmph  23783  nrmhmph  23784  filconn  23873  trfil1  23876  ufildr  23921  flimfil  23959  flimfnfcls  24018  alexsublem  24034  alexsubALTlem3  24039  ustbas2  24215  tgioo  24786  xrtgioo  24797  xrsmopn  24803  opnreen  24822  cnheibor  24947  cnllycmp  24948  lebnumlem1  24953  lebnumlem3  24955  bcthlem5  25320  bcth3  25323  voliunlem1  25542  voliunlem3  25544  volsup  25548  opnmbllem  25593  mbfimaopnlem  25647  lhop  26008  nosupno  27692  noinfno  27707  noetasuplem4  27725  noetainflem4  27729  tglnpt  28642  tglineintmo  28735  ubthlem1  30966  shatomistici  32457  hatomistici  32458  elrspunidl  33518  zarclsiin  34062  tpr2rico  34103  hasheuni  34276  difelsiga  34324  prob01  34604  probdsb  34613  totprobd  34617  probmeasb  34621  cndprobtot  34627  orvcelval  34660  bnj1450  35239  bnj1501  35256  elwf  35285  pconnconn  35466  cvmsf1o  35507  cvmscld  35508  cvmsss2  35509  cvmopnlem  35513  cvmfolem  35514  cvmliftmolem1  35516  cvmliftlem6  35525  cvmliftlem8  35527  cvmlift2lem9  35546  cvmlift2lem11  35548  cvmlift2lem12  35549  cvmlift3lem6  35559  dfon2lem3  36018  dfon2lem7  36022  ntruni  36562  clsint2  36564  neibastop1  36594  topmeet  36599  topjoin  36600  fnemeet1  36601  fnejoin1  36603  dfttc2g  36741  opnmbllem0  38030  mbfresfi  38040  heiborlem1  38185  lssats  39511  dicval  41675  mapdunirnN  42149  isnacs3  43166  aomclem4  43509  kelac2  43517  onsupuni  43681  onsupmaxb  43691  mnuunid  44728  mnutrcld  44730  grumnudlem  44736  wfac8prim  45453  ssuniint  45533  stoweidlem28  46478  stoweidlem50  46500  stoweidlem52  46502  stoweidlem53  46503  stoweidlem54  46504  prsal  46768  salincl  46774  saliinclf  46776  saldifcl2  46778  salexct  46784  psmeasurelem  46920  caragenuni  46961  carageniuncl  46973  caratheodorylem1  46976  caratheodorylem2  46977  voncmpl  47071  opncldeqv  49399  opndisj  49400  unilbeu  49482  setrec1lem2  50185  setrec2fun  50189