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

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3962  ∪ cuni 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-uni 4912

This theorem is referenced by:  unissel  4942  ssunieq  4947  pwuni  4949  pwel  5386  uniopel  5525  dmrnssfld  5986  unixp0  6304  elfvunirn  6938  fvssunirnOLD  6940  sorpssuni  7750  iunpw  7789  pwuninel2  8297  frrlem8  8316  frrlem10  8318  frrlem14  8322  fprresex  8333  wfrlem12OLD  8358  wfrlem16OLD  8362  wfrlem17OLD  8363  onfununi  8379  tfrlem9  8423  tfrlem9a  8424  tfrlem13  8428  sbthlem1  9121  sbthlem2  9122  2pwuninel  9170  ordunifi  9323  unifpw  9392  fissuni  9394  dffi3  9468  cantnfp1lem3  9717  oemapvali  9721  cantnflem1  9726  cnfcom3lem  9740  rankuni2b  9890  carduni  10018  r0weon  10049  dfac8clem  10069  cardinfima  10134  alephfp  10145  iunfictbso  10151  dfac5lem4  10163  dfac5lem4OLD  10165  dfac2a  10167  dfacacn  10179  dfac12lem2  10182  kmlem2  10189  fin23lem16  10372  fin23lem21  10376  isf32lem5  10394  fin1a2lem11  10447  fin1a2lem13  10449  itunitc  10458  axdc2lem  10485  axdc3lem2  10488  ttukeylem5  10550  ttukeylem6  10551  fpwwe2lem10  10677  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  wunex2  10775  inatsk  10815  tskuni  10820  suplem1pr  11089  suplem2pr  11090  unirnioo  13485  mrcuni  17665  isacs3lem  18599  mrelatlub  18619  dprd2dlem1  20075  lbsextlem2  21178  eltopss  22928  toponss  22948  isbasis3g  22971  baspartn  22976  bastg  22988  tgcl  22991  fctop  23026  cctop  23028  ppttop  23029  epttop  23031  difopn  23057  ssntr  23081  isopn3  23089  isopn3i  23105  toponmre  23116  neiuni  23145  neiptoptop  23154  resttopon  23184  restopn2  23200  perfopn  23208  pnfnei  23243  mnfnei  23244  ssidcn  23278  lmcnp  23327  pnrmopn  23366  ist1-2  23370  nrmsep  23380  isnrm2  23381  isnrm3  23382  regsep2  23399  cncmp  23415  hauscmplem  23429  hauscmp  23430  conndisj  23439  cnconn  23445  conncompss  23456  islly2  23507  nllyrest  23509  nllyidm  23512  hausllycmp  23517  cldllycmp  23518  lly1stc  23519  comppfsc  23555  kgentopon  23561  kgenss  23566  llycmpkgen2  23573  1stckgen  23577  txuni2  23588  ptpjpre1  23594  ptuni2  23599  ptbasfi  23604  xkouni  23622  txcnpi  23631  ptpjopn  23635  txindis  23657  txnlly  23660  txtube  23663  hausdiag  23668  xkopt  23678  xkococnlem  23682  txconn  23712  qtopuni  23725  qtopkgen  23733  tgqtop  23735  regr1lem  23762  kqreglem1  23764  kqreglem2  23765  kqnrmlem1  23766  kqnrmlem2  23767  hmeoimaf1o  23793  reghmph  23816  nrmhmph  23817  filconn  23906  trfil1  23909  ufildr  23954  flimfil  23992  flimfnfcls  24051  alexsublem  24067  alexsubALTlem3  24072  ustbas2  24249  tgioo  24831  xrtgioo  24841  xrsmopn  24847  opnreen  24866  cnheibor  25000  cnllycmp  25001  lebnumlem1  25006  lebnumlem3  25008  bcthlem5  25375  bcth3  25378  voliunlem1  25598  voliunlem3  25600  volsup  25604  opnmbllem  25649  mbfimaopnlem  25703  lhop  26069  nosupno  27762  noinfno  27777  noetasuplem4  27795  noetainflem4  27799  tglnpt  28571  tglineintmo  28664  ubthlem1  30898  shatomistici  32389  hatomistici  32390  unifi3  32729  elrspunidl  33435  zarclsiin  33831  tpr2rico  33872  hasheuni  34065  difelsiga  34113  prob01  34394  probdsb  34403  totprobd  34407  probmeasb  34411  cndprobtot  34417  orvcelval  34449  bnj1450  35042  bnj1501  35059  pconnconn  35215  cvmsf1o  35256  cvmscld  35257  cvmsss2  35258  cvmopnlem  35262  cvmfolem  35263  cvmliftmolem1  35265  cvmliftlem6  35274  cvmliftlem8  35276  cvmlift2lem9  35295  cvmlift2lem11  35297  cvmlift2lem12  35298  cvmlift3lem6  35308  dfon2lem3  35766  dfon2lem7  35770  ntruni  36309  clsint2  36311  neibastop1  36341  topmeet  36346  topjoin  36347  fnemeet1  36348  fnejoin1  36350  opnmbllem0  37642  mbfresfi  37652  heiborlem1  37797  lssats  38993  dicval  41158  mapdunirnN  41632  isnacs3  42697  aomclem4  43045  kelac2  43053  onsupuni  43217  onsupmaxb  43227  mnuunid  44272  mnutrcld  44274  grumnudlem  44280  ssuniint  45017  stoweidlem28  45983  stoweidlem50  46005  stoweidlem52  46007  stoweidlem53  46008  stoweidlem54  46009  prsal  46273  salincl  46279  saliinclf  46281  saldifcl2  46283  salexct  46289  psmeasurelem  46425  caragenuni  46466  carageniuncl  46478  caratheodorylem1  46481  caratheodorylem2  46482  voncmpl  46576  opncldeqv  48697  opndisj  48698  unilbeu  48773  setrec1lem2  48918  setrec2fun  48922