Theorem elssuni 4937

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3951  ∪ cuni 4907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908

This theorem is referenced by:  unissel  4938  ssunieq  4943  pwuni  4945  pwel  5381  uniopel  5521  dmrnssfld  5984  unixp0  6303  elfvunirn  6938  fvssunirnOLD  6940  sorpssuni  7752  iunpw  7791  pwuninel2  8299  frrlem8  8318  frrlem10  8320  frrlem14  8324  fprresex  8335  wfrlem12OLD  8360  wfrlem16OLD  8364  wfrlem17OLD  8365  onfununi  8381  tfrlem9  8425  tfrlem9a  8426  tfrlem13  8430  sbthlem1  9123  sbthlem2  9124  2pwuninel  9172  ordunifi  9326  unifpw  9395  fissuni  9397  dffi3  9471  cantnfp1lem3  9720  oemapvali  9724  cantnflem1  9729  cnfcom3lem  9743  rankuni2b  9893  carduni  10021  r0weon  10052  dfac8clem  10072  cardinfima  10137  alephfp  10148  iunfictbso  10154  dfac5lem4  10166  dfac5lem4OLD  10168  dfac2a  10170  dfacacn  10182  dfac12lem2  10185  kmlem2  10192  fin23lem16  10375  fin23lem21  10379  isf32lem5  10397  fin1a2lem11  10450  fin1a2lem13  10452  itunitc  10461  axdc2lem  10488  axdc3lem2  10491  ttukeylem5  10553  ttukeylem6  10554  fpwwe2lem10  10680  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe2  10683  wunex2  10778  inatsk  10818  tskuni  10823  suplem1pr  11092  suplem2pr  11093  unirnioo  13489  mrcuni  17664  isacs3lem  18587  mrelatlub  18607  dprd2dlem1  20061  lbsextlem2  21161  eltopss  22913  toponss  22933  isbasis3g  22956  baspartn  22961  bastg  22973  tgcl  22976  fctop  23011  cctop  23013  ppttop  23014  epttop  23016  difopn  23042  ssntr  23066  isopn3  23074  isopn3i  23090  toponmre  23101  neiuni  23130  neiptoptop  23139  resttopon  23169  restopn2  23185  perfopn  23193  pnfnei  23228  mnfnei  23229  ssidcn  23263  lmcnp  23312  pnrmopn  23351  ist1-2  23355  nrmsep  23365  isnrm2  23366  isnrm3  23367  regsep2  23384  cncmp  23400  hauscmplem  23414  hauscmp  23415  conndisj  23424  cnconn  23430  conncompss  23441  islly2  23492  nllyrest  23494  nllyidm  23497  hausllycmp  23502  cldllycmp  23503  lly1stc  23504  comppfsc  23540  kgentopon  23546  kgenss  23551  llycmpkgen2  23558  1stckgen  23562  txuni2  23573  ptpjpre1  23579  ptuni2  23584  ptbasfi  23589  xkouni  23607  txcnpi  23616  ptpjopn  23620  txindis  23642  txnlly  23645  txtube  23648  hausdiag  23653  xkopt  23663  xkococnlem  23667  txconn  23697  qtopuni  23710  qtopkgen  23718  tgqtop  23720  regr1lem  23747  kqreglem1  23749  kqreglem2  23750  kqnrmlem1  23751  kqnrmlem2  23752  hmeoimaf1o  23778  reghmph  23801  nrmhmph  23802  filconn  23891  trfil1  23894  ufildr  23939  flimfil  23977  flimfnfcls  24036  alexsublem  24052  alexsubALTlem3  24057  ustbas2  24234  tgioo  24817  xrtgioo  24828  xrsmopn  24834  opnreen  24853  cnheibor  24987  cnllycmp  24988  lebnumlem1  24993  lebnumlem3  24995  bcthlem5  25362  bcth3  25365  voliunlem1  25585  voliunlem3  25587  volsup  25591  opnmbllem  25636  mbfimaopnlem  25690  lhop  26055  nosupno  27748  noinfno  27763  noetasuplem4  27781  noetainflem4  27785  tglnpt  28557  tglineintmo  28650  ubthlem1  30889  shatomistici  32380  hatomistici  32381  unifi3  32724  elrspunidl  33456  zarclsiin  33870  tpr2rico  33911  hasheuni  34086  difelsiga  34134  prob01  34415  probdsb  34424  totprobd  34428  probmeasb  34432  cndprobtot  34438  orvcelval  34471  bnj1450  35064  bnj1501  35081  pconnconn  35236  cvmsf1o  35277  cvmscld  35278  cvmsss2  35279  cvmopnlem  35283  cvmfolem  35284  cvmliftmolem1  35286  cvmliftlem6  35295  cvmliftlem8  35297  cvmlift2lem9  35316  cvmlift2lem11  35318  cvmlift2lem12  35319  cvmlift3lem6  35329  dfon2lem3  35786  dfon2lem7  35790  ntruni  36328  clsint2  36330  neibastop1  36360  topmeet  36365  topjoin  36366  fnemeet1  36367  fnejoin1  36369  opnmbllem0  37663  mbfresfi  37673  heiborlem1  37818  lssats  39013  dicval  41178  mapdunirnN  41652  isnacs3  42721  aomclem4  43069  kelac2  43077  onsupuni  43241  onsupmaxb  43251  mnuunid  44296  mnutrcld  44298  grumnudlem  44304  wfac8prim  45019  ssuniint  45083  stoweidlem28  46043  stoweidlem50  46065  stoweidlem52  46067  stoweidlem53  46068  stoweidlem54  46069  prsal  46333  salincl  46339  saliinclf  46341  saldifcl2  46343  salexct  46349  psmeasurelem  46485  caragenuni  46526  carageniuncl  46538  caratheodorylem1  46541  caratheodorylem2  46542  voncmpl  46636  opncldeqv  48799  opndisj  48800  unilbeu  48874  setrec1lem2  49207  setrec2fun  49211