Theorem elssuni 4941

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

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3948  ∪ cuni 4908

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965  df-uni 4909

This theorem is referenced by:  unissel  4942  ssunieq  4947  pwuni  4949  pwel  5379  uniopel  5516  dmrnssfld  5969  unixp0  6282  elfvunirn  6923  fvssunirnOLD  6925  sorpssuni  7726  iunpw  7762  pwuninel2  8265  frrlem8  8284  frrlem10  8286  frrlem14  8290  fprresex  8301  wfrlem12OLD  8326  wfrlem16OLD  8330  wfrlem17OLD  8331  onfununi  8347  tfrlem9  8391  tfrlem9a  8392  tfrlem13  8396  sbthlem1  9089  sbthlem2  9090  2pwuninel  9138  ordunifi  9299  unifpw  9361  fissuni  9363  dffi3  9432  cantnfp1lem3  9681  oemapvali  9685  cantnflem1  9690  cnfcom3lem  9704  rankuni2b  9854  carduni  9982  r0weon  10013  dfac8clem  10033  cardinfima  10098  alephfp  10109  iunfictbso  10115  dfac5lem4  10127  dfac2a  10130  dfacacn  10142  dfac12lem2  10145  kmlem2  10152  fin23lem16  10336  fin23lem21  10340  isf32lem5  10358  fin1a2lem11  10411  fin1a2lem13  10413  itunitc  10422  axdc2lem  10449  axdc3lem2  10452  ttukeylem5  10514  ttukeylem6  10515  fpwwe2lem10  10641  fpwwe2lem11  10642  fpwwe2lem12  10643  fpwwe2  10644  wunex2  10739  inatsk  10779  tskuni  10784  suplem1pr  11053  suplem2pr  11054  unirnioo  13433  mrcuni  17572  isacs3lem  18505  mrelatlub  18525  dprd2dlem1  19959  lbsextlem2  21005  eltopss  22728  toponss  22748  isbasis3g  22771  baspartn  22776  bastg  22788  tgcl  22791  fctop  22826  cctop  22828  ppttop  22829  epttop  22831  difopn  22857  ssntr  22881  isopn3  22889  isopn3i  22905  toponmre  22916  neiuni  22945  neiptoptop  22954  resttopon  22984  restopn2  23000  perfopn  23008  pnfnei  23043  mnfnei  23044  ssidcn  23078  lmcnp  23127  pnrmopn  23166  ist1-2  23170  nrmsep  23180  isnrm2  23181  isnrm3  23182  regsep2  23199  cncmp  23215  hauscmplem  23229  hauscmp  23230  conndisj  23239  cnconn  23245  conncompss  23256  islly2  23307  nllyrest  23309  nllyidm  23312  hausllycmp  23317  cldllycmp  23318  lly1stc  23319  comppfsc  23355  kgentopon  23361  kgenss  23366  llycmpkgen2  23373  1stckgen  23377  txuni2  23388  ptpjpre1  23394  ptuni2  23399  ptbasfi  23404  xkouni  23422  txcnpi  23431  ptpjopn  23435  txindis  23457  txnlly  23460  txtube  23463  hausdiag  23468  xkopt  23478  xkococnlem  23482  txconn  23512  qtopuni  23525  qtopkgen  23533  tgqtop  23535  regr1lem  23562  kqreglem1  23564  kqreglem2  23565  kqnrmlem1  23566  kqnrmlem2  23567  hmeoimaf1o  23593  reghmph  23616  nrmhmph  23617  filconn  23706  trfil1  23709  ufildr  23754  flimfil  23792  flimfnfcls  23851  alexsublem  23867  alexsubALTlem3  23872  ustbas2  24049  tgioo  24631  xrtgioo  24641  xrsmopn  24647  opnreen  24666  cnheibor  24800  cnllycmp  24801  lebnumlem1  24806  lebnumlem3  24808  bcthlem5  25175  bcth3  25178  voliunlem1  25398  voliunlem3  25400  volsup  25404  opnmbllem  25449  mbfimaopnlem  25503  lhop  25868  nosupno  27548  noinfno  27563  noetasuplem4  27581  noetainflem4  27585  tglnpt  28232  tglineintmo  28325  ubthlem1  30555  shatomistici  32046  hatomistici  32047  unifi3  32369  elrspunidl  32985  zarclsiin  33314  tpr2rico  33355  hasheuni  33546  difelsiga  33594  prob01  33875  probdsb  33884  totprobd  33888  probmeasb  33892  cndprobtot  33898  orvcelval  33930  bnj1450  34524  bnj1501  34541  pconnconn  34685  cvmsf1o  34726  cvmscld  34727  cvmsss2  34728  cvmopnlem  34732  cvmfolem  34733  cvmliftmolem1  34735  cvmliftlem6  34744  cvmliftlem8  34746  cvmlift2lem9  34765  cvmlift2lem11  34767  cvmlift2lem12  34768  cvmlift3lem6  34778  dfon2lem3  35226  dfon2lem7  35230  ntruni  35675  clsint2  35677  neibastop1  35707  topmeet  35712  topjoin  35713  fnemeet1  35714  fnejoin1  35716  opnmbllem0  36987  mbfresfi  36997  heiborlem1  37142  lssats  38345  dicval  40510  mapdunirnN  40984  isnacs3  41910  aomclem4  42261  kelac2  42269  onsupuni  42440  onsupmaxb  42450  mnuunid  43498  mnutrcld  43500  grumnudlem  43506  ssuniint  44228  stoweidlem28  45202  stoweidlem50  45224  stoweidlem52  45226  stoweidlem53  45227  stoweidlem54  45228  prsal  45492  salincl  45498  saliinclf  45500  saldifcl2  45502  salexct  45508  psmeasurelem  45644  caragenuni  45685  carageniuncl  45697  caratheodorylem1  45700  caratheodorylem2  45701  voncmpl  45795  opncldeqv  47695  opndisj  47696  unilbeu  47771  setrec1lem2  47894  setrec2fun  47898