Theorem elssuni 4870

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3938  ∪ cuni 4840

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-in 3945  df-ss 3954  df-uni 4841

This theorem is referenced by:  unissel  4871  ssunieq  4875  pwuni  4877  pwel  5284  uniopel  5408  dmrnssfld  5843  unixp0  6136  fvssunirn  6701  sorpssuni  7460  iunpw  7495  pwuninel2  7942  wfrlem12  7968  wfrlem16  7972  wfrlem17  7973  onfununi  7980  tfrlem9  8023  tfrlem9a  8024  tfrlem13  8028  sbthlem1  8629  sbthlem2  8630  2pwuninel  8674  ordunifi  8770  unifpw  8829  fissuni  8831  dffi3  8897  cantnfp1lem3  9145  oemapvali  9149  cantnflem1  9154  cnfcom3lem  9168  rankuni2b  9284  carduni  9412  r0weon  9440  dfac8clem  9460  cardinfima  9525  alephfp  9536  iunfictbso  9542  dfac5lem4  9554  dfac2a  9557  dfacacn  9569  dfac12lem2  9572  kmlem2  9579  fin23lem16  9759  fin23lem21  9763  isf32lem5  9781  fin1a2lem11  9834  fin1a2lem13  9836  itunitc  9845  axdc2lem  9872  axdc3lem2  9875  ttukeylem5  9937  ttukeylem6  9938  fpwwe2lem11  10064  fpwwe2lem12  10065  fpwwe2lem13  10066  fpwwe2  10067  wunex2  10162  inatsk  10202  tskuni  10207  suplem1pr  10476  suplem2pr  10477  unirnioo  12840  mrcuni  16894  isacs3lem  17778  mrelatlub  17798  dprd2dlem1  19165  lbsextlem2  19933  eltopss  21517  toponss  21537  isbasis3g  21559  baspartn  21564  bastg  21576  tgcl  21579  fctop  21614  cctop  21616  ppttop  21617  epttop  21619  difopn  21644  ssntr  21668  isopn3  21676  isopn3i  21692  toponmre  21703  neiuni  21732  neiptoptop  21741  resttopon  21771  restopn2  21787  perfopn  21795  pnfnei  21830  mnfnei  21831  ssidcn  21865  lmcnp  21914  pnrmopn  21953  ist1-2  21957  nrmsep  21967  isnrm2  21968  isnrm3  21969  regsep2  21986  cncmp  22002  hauscmplem  22016  hauscmp  22017  conndisj  22026  cnconn  22032  conncompss  22043  islly2  22094  nllyrest  22096  nllyidm  22099  hausllycmp  22104  cldllycmp  22105  lly1stc  22106  comppfsc  22142  kgentopon  22148  kgenss  22153  llycmpkgen2  22160  1stckgen  22164  txuni2  22175  ptpjpre1  22181  ptuni2  22186  ptbasfi  22191  xkouni  22209  txcnpi  22218  ptpjopn  22222  txindis  22244  txnlly  22247  txtube  22250  hausdiag  22255  xkopt  22265  xkococnlem  22269  txconn  22299  qtopuni  22312  qtopkgen  22320  tgqtop  22322  regr1lem  22349  kqreglem1  22351  kqreglem2  22352  kqnrmlem1  22353  kqnrmlem2  22354  hmeoimaf1o  22380  reghmph  22403  nrmhmph  22404  filconn  22493  trfil1  22496  ufildr  22541  flimfil  22579  flimfnfcls  22638  alexsublem  22654  alexsubALTlem3  22659  ustbas2  22836  tgioo  23406  xrtgioo  23416  xrsmopn  23422  opnreen  23441  cnheibor  23561  cnllycmp  23562  lebnumlem1  23567  lebnumlem3  23569  bcthlem5  23933  bcth3  23936  voliunlem1  24153  voliunlem3  24155  volsup  24159  opnmbllem  24204  mbfimaopnlem  24258  lhop  24615  tglnpt  26337  tglineintmo  26430  ubthlem1  28649  shatomistici  30140  hatomistici  30141  unifi3  30450  tpr2rico  31157  hasheuni  31346  difelsiga  31394  prob01  31673  probdsb  31682  totprobd  31686  probmeasb  31690  cndprobtot  31696  orvcelval  31728  bnj1450  32324  bnj1501  32341  pconnconn  32480  cvmsf1o  32521  cvmscld  32522  cvmsss2  32523  cvmopnlem  32527  cvmfolem  32528  cvmliftmolem1  32530  cvmliftlem6  32539  cvmliftlem8  32541  cvmlift2lem9  32560  cvmlift2lem11  32562  cvmlift2lem12  32563  cvmlift3lem6  32573  dfon2lem3  33032  dfon2lem7  33036  trpredpred  33069  frrlem8  33132  frrlem10  33134  frrlem14  33138  nosupno  33205  nosupbday  33207  noetalem3  33221  ntruni  33677  clsint2  33679  neibastop1  33709  topmeet  33714  topjoin  33715  fnemeet1  33716  fnejoin1  33718  opnmbllem0  34930  mbfresfi  34940  heiborlem1  35091  lssats  36150  dicval  38314  mapdunirnN  38788  isnacs3  39314  aomclem4  39664  kelac2  39672  mnuunid  40620  mnutrcld  40622  grumnudlem  40628  ssuniint  41349  stoweidlem28  42320  stoweidlem50  42342  stoweidlem52  42344  stoweidlem53  42345  stoweidlem54  42346  prsal  42610  salincl  42615  saliincl  42617  saldifcl2  42618  salexct  42624  psmeasurelem  42759  caragenuni  42800  carageniuncl  42812  caratheodorylem1  42815  caratheodorylem2  42816  voncmpl  42910  setrec1lem2  44798  setrec2fun  44802