Theorem elssuni 4940

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

Syntax hints:   → wi 4   ∈ wcel 2104   ⊆ wss 3947  ∪ 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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-uni 4908

This theorem is referenced by:  unissel  4941  ssunieq  4946  pwuni  4948  pwel  5378  uniopel  5515  dmrnssfld  5968  unixp0  6281  elfvunirn  6922  fvssunirnOLD  6924  sorpssuni  7724  iunpw  7760  pwuninel2  8261  frrlem8  8280  frrlem10  8282  frrlem14  8286  fprresex  8297  wfrlem12OLD  8322  wfrlem16OLD  8326  wfrlem17OLD  8327  onfununi  8343  tfrlem9  8387  tfrlem9a  8388  tfrlem13  8392  sbthlem1  9085  sbthlem2  9086  2pwuninel  9134  ordunifi  9295  unifpw  9357  fissuni  9359  dffi3  9428  cantnfp1lem3  9677  oemapvali  9681  cantnflem1  9686  cnfcom3lem  9700  rankuni2b  9850  carduni  9978  r0weon  10009  dfac8clem  10029  cardinfima  10094  alephfp  10105  iunfictbso  10111  dfac5lem4  10123  dfac2a  10126  dfacacn  10138  dfac12lem2  10141  kmlem2  10148  fin23lem16  10332  fin23lem21  10336  isf32lem5  10354  fin1a2lem11  10407  fin1a2lem13  10409  itunitc  10418  axdc2lem  10445  axdc3lem2  10448  ttukeylem5  10510  ttukeylem6  10511  fpwwe2lem10  10637  fpwwe2lem11  10638  fpwwe2lem12  10639  fpwwe2  10640  wunex2  10735  inatsk  10775  tskuni  10780  suplem1pr  11049  suplem2pr  11050  unirnioo  13430  mrcuni  17569  isacs3lem  18499  mrelatlub  18519  dprd2dlem1  19952  lbsextlem2  20917  eltopss  22629  toponss  22649  isbasis3g  22672  baspartn  22677  bastg  22689  tgcl  22692  fctop  22727  cctop  22729  ppttop  22730  epttop  22732  difopn  22758  ssntr  22782  isopn3  22790  isopn3i  22806  toponmre  22817  neiuni  22846  neiptoptop  22855  resttopon  22885  restopn2  22901  perfopn  22909  pnfnei  22944  mnfnei  22945  ssidcn  22979  lmcnp  23028  pnrmopn  23067  ist1-2  23071  nrmsep  23081  isnrm2  23082  isnrm3  23083  regsep2  23100  cncmp  23116  hauscmplem  23130  hauscmp  23131  conndisj  23140  cnconn  23146  conncompss  23157  islly2  23208  nllyrest  23210  nllyidm  23213  hausllycmp  23218  cldllycmp  23219  lly1stc  23220  comppfsc  23256  kgentopon  23262  kgenss  23267  llycmpkgen2  23274  1stckgen  23278  txuni2  23289  ptpjpre1  23295  ptuni2  23300  ptbasfi  23305  xkouni  23323  txcnpi  23332  ptpjopn  23336  txindis  23358  txnlly  23361  txtube  23364  hausdiag  23369  xkopt  23379  xkococnlem  23383  txconn  23413  qtopuni  23426  qtopkgen  23434  tgqtop  23436  regr1lem  23463  kqreglem1  23465  kqreglem2  23466  kqnrmlem1  23467  kqnrmlem2  23468  hmeoimaf1o  23494  reghmph  23517  nrmhmph  23518  filconn  23607  trfil1  23610  ufildr  23655  flimfil  23693  flimfnfcls  23752  alexsublem  23768  alexsubALTlem3  23773  ustbas2  23950  tgioo  24532  xrtgioo  24542  xrsmopn  24548  opnreen  24567  cnheibor  24701  cnllycmp  24702  lebnumlem1  24707  lebnumlem3  24709  bcthlem5  25076  bcth3  25079  voliunlem1  25299  voliunlem3  25301  volsup  25305  opnmbllem  25350  mbfimaopnlem  25404  lhop  25768  nosupno  27442  noinfno  27457  noetasuplem4  27475  noetainflem4  27479  tglnpt  28067  tglineintmo  28160  ubthlem1  30390  shatomistici  31881  hatomistici  31882  unifi3  32204  elrspunidl  32820  zarclsiin  33149  tpr2rico  33190  hasheuni  33381  difelsiga  33429  prob01  33710  probdsb  33719  totprobd  33723  probmeasb  33727  cndprobtot  33733  orvcelval  33765  bnj1450  34359  bnj1501  34376  pconnconn  34520  cvmsf1o  34561  cvmscld  34562  cvmsss2  34563  cvmopnlem  34567  cvmfolem  34568  cvmliftmolem1  34570  cvmliftlem6  34579  cvmliftlem8  34581  cvmlift2lem9  34600  cvmlift2lem11  34602  cvmlift2lem12  34603  cvmlift3lem6  34613  dfon2lem3  35061  dfon2lem7  35065  ntruni  35515  clsint2  35517  neibastop1  35547  topmeet  35552  topjoin  35553  fnemeet1  35554  fnejoin1  35556  opnmbllem0  36827  mbfresfi  36837  heiborlem1  36982  lssats  38185  dicval  40350  mapdunirnN  40824  isnacs3  41750  aomclem4  42101  kelac2  42109  onsupuni  42280  onsupmaxb  42290  mnuunid  43338  mnutrcld  43340  grumnudlem  43346  ssuniint  44068  stoweidlem28  45042  stoweidlem50  45064  stoweidlem52  45066  stoweidlem53  45067  stoweidlem54  45068  prsal  45332  salincl  45338  saliinclf  45340  saldifcl2  45342  salexct  45348  psmeasurelem  45484  caragenuni  45525  carageniuncl  45537  caratheodorylem1  45540  caratheodorylem2  45541  voncmpl  45635  opncldeqv  47621  opndisj  47622  unilbeu  47697  setrec1lem2  47820  setrec2fun  47824