Theorem elssuni 4690

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

Syntax hints:   → wi 4   ∈ wcel 2166   ⊆ wss 3799  ∪ cuni 4659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-v 3417  df-in 3806  df-ss 3813  df-uni 4660

This theorem is referenced by:  unissel  4691  ssunieq  4695  pwuni  4697  pwel  5142  uniopel  5203  dmrnssfld  5618  unixp0  5911  fvssunirn  6463  sorpssuni  7207  iunpw  7240  pwuninel2  7666  wfrlem12  7693  wfrlem16  7697  wfrlem17  7698  onfununi  7705  tfrlem9  7748  tfrlem9a  7749  tfrlem13  7753  sbthlem1  8340  sbthlem2  8341  2pwuninel  8385  ordunifi  8480  unifpw  8539  fissuni  8541  dffi3  8607  cantnfp1lem3  8855  oemapvali  8859  cantnflem1  8864  cnfcom3lem  8878  rankuni2b  8994  carduni  9121  r0weon  9149  dfac8clem  9169  cardinfima  9234  alephfp  9245  iunfictbso  9251  dfac5lem4  9263  dfac2a  9266  dfacacn  9279  dfac12lem2  9282  kmlem2  9289  fin23lem16  9473  fin23lem21  9477  isf32lem5  9495  fin1a2lem11  9548  fin1a2lem13  9550  itunitc  9559  axdc2lem  9586  axdc3lem2  9589  ttukeylem5  9651  ttukeylem6  9652  fpwwe2lem11  9778  fpwwe2lem12  9779  fpwwe2lem13  9780  fpwwe2  9781  wunex2  9876  inatsk  9916  tskuni  9921  suplem1pr  10190  suplem2pr  10191  unirnioo  12563  mrcuni  16635  isacs3lem  17520  mrelatlub  17540  dprd2dlem1  18795  lbsextlem2  19521  eltopss  21083  toponss  21103  isbasis3g  21125  baspartn  21130  bastg  21142  tgcl  21145  fctop  21180  cctop  21182  ppttop  21183  epttop  21185  difopn  21210  ssntr  21234  isopn3  21242  isopn3i  21258  toponmre  21269  neiuni  21298  neiptoptop  21307  resttopon  21337  restopn2  21353  perfopn  21361  pnfnei  21396  mnfnei  21397  ssidcn  21431  lmcnp  21480  pnrmopn  21519  ist1-2  21523  nrmsep  21533  isnrm2  21534  isnrm3  21535  regsep2  21552  cncmp  21567  hauscmplem  21581  hauscmp  21582  conndisj  21591  cnconn  21597  conncompss  21608  islly2  21659  nllyrest  21661  nllyidm  21664  hausllycmp  21669  cldllycmp  21670  lly1stc  21671  comppfsc  21707  kgentopon  21713  kgenss  21718  llycmpkgen2  21725  1stckgen  21729  txuni2  21740  ptpjpre1  21746  ptuni2  21751  ptbasfi  21756  xkouni  21774  txcnpi  21783  ptpjopn  21787  txindis  21809  txnlly  21812  txtube  21815  hausdiag  21820  xkopt  21830  xkococnlem  21834  txconn  21864  qtopuni  21877  qtopkgen  21885  tgqtop  21887  regr1lem  21914  kqreglem1  21916  kqreglem2  21917  kqnrmlem1  21918  kqnrmlem2  21919  hmeoimaf1o  21945  reghmph  21968  nrmhmph  21969  filconn  22058  trfil1  22061  ufildr  22106  flimfil  22144  flimfnfcls  22203  alexsublem  22219  alexsubALTlem3  22224  ustbas2  22400  tgioo  22970  xrtgioo  22980  xrsmopn  22986  opnreen  23005  cnheibor  23125  cnllycmp  23126  lebnumlem1  23131  lebnumlem3  23133  bcthlem5  23497  bcth3  23500  voliunlem1  23717  voliunlem3  23719  volsup  23723  opnmbllem  23768  mbfimaopnlem  23822  lhop  24179  tglnpt  25862  tglineintmo  25955  ubthlem1  28282  shatomistici  29776  hatomistici  29777  unifi3  30039  tpr2rico  30504  hasheuni  30693  difelsiga  30742  prob01  31022  probdsb  31031  totprobd  31035  probmeasb  31039  cndprobtot  31045  orvcelval  31077  bnj1450  31665  bnj1501  31682  pconnconn  31760  cvmsf1o  31801  cvmscld  31802  cvmsss2  31803  cvmopnlem  31807  cvmfolem  31808  cvmliftmolem1  31810  cvmliftlem6  31819  cvmliftlem8  31821  cvmlift2lem9  31840  cvmlift2lem11  31842  cvmlift2lem12  31843  cvmlift3lem6  31853  dfon2lem3  32229  dfon2lem7  32233  trpredpred  32267  frrlem11  32332  nosupno  32389  nosupbday  32391  noetalem3  32405  ntruni  32861  clsint2  32863  neibastop1  32893  topmeet  32898  topjoin  32899  fnemeet1  32900  fnejoin1  32902  opnmbllem0  33990  mbfresfi  34000  heiborlem1  34153  lssats  35088  dicval  37252  mapdunirnN  37726  isnacs3  38118  aomclem4  38471  kelac2  38479  ssuniint  40068  stoweidlem28  41040  stoweidlem50  41062  stoweidlem52  41064  stoweidlem53  41065  stoweidlem54  41066  prsal  41330  salincl  41335  saliincl  41337  saldifcl2  41338  salexct  41344  psmeasurelem  41479  caragenuni  41520  carageniuncl  41532  caratheodorylem1  41535  caratheodorylem2  41536  voncmpl  41630  setrec1lem2  43331  setrec2fun  43335