Theorem elssuni 4403

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

Syntax hints:   → wi 4   ∈ wcel 1977   ⊆ wss 3540  ∪ cuni 4372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-uni 4373

This theorem is referenced by:  unissel  4404  ssunieq  4408  pwuni  4825  pwel  4847  uniopel  4903  dmrnssfld  5305  unixp0  5586  fvssunirn  6127  sorpssuni  6844  iunpw  6870  pwuninel2  7287  wfrlem12  7313  wfrlem16  7317  wfrlem17  7318  onfununi  7325  tfrlem9  7368  tfrlem9a  7369  tfrlem13  7373  sbthlem1  7955  sbthlem2  7956  2pwuninel  8000  ordunifi  8095  unifpw  8152  fissuni  8154  dffi3  8220  cantnfp1lem3  8460  oemapvali  8464  cantnflem1  8469  cnfcom3lem  8483  rankuni2b  8599  carduni  8690  r0weon  8718  dfac8clem  8738  cardinfima  8803  alephfp  8814  iunfictbso  8820  dfac5lem4  8832  dfac2a  8835  dfacacn  8846  dfac12lem2  8849  kmlem2  8856  fin23lem16  9040  fin23lem21  9044  isf32lem5  9062  fin1a2lem11  9115  fin1a2lem13  9117  itunitc  9126  axdc2lem  9153  axdc3lem2  9156  ttukeylem5  9218  ttukeylem6  9219  fpwwe2lem11  9341  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwe2  9344  wunex2  9439  inatsk  9479  tskuni  9484  suplem1pr  9753  suplem2pr  9754  unirnioo  12144  mrcuni  16104  isacs3lem  16989  mrelatlub  17009  dprd2dlem1  18263  lbsextlem2  18980  eltopss  20537  toponss  20544  isbasis3g  20564  baspartn  20569  bastg  20581  tgcl  20584  fctop  20618  cctop  20620  ppttop  20621  epttop  20623  difopn  20648  ssntr  20672  isopn3  20680  isopn3i  20696  toponmre  20707  neiuni  20736  neiptoptop  20745  resttopon  20775  restopn2  20791  perfopn  20799  pnfnei  20834  mnfnei  20835  ssidcn  20869  lmcnp  20918  pnrmopn  20957  ist1-2  20961  nrmsep  20971  isnrm2  20972  isnrm3  20973  regsep2  20990  cncmp  21005  hauscmplem  21019  hauscmp  21020  conndisj  21029  cnconn  21035  concompss  21046  islly2  21097  nllyrest  21099  nllyidm  21102  hausllycmp  21107  cldllycmp  21108  lly1stc  21109  comppfsc  21145  kgentopon  21151  kgenss  21156  llycmpkgen2  21163  1stckgen  21167  txuni2  21178  ptpjpre1  21184  ptuni2  21189  ptbasfi  21194  xkouni  21212  txcnpi  21221  ptpjopn  21225  txindis  21247  txnlly  21250  txtube  21253  hausdiag  21258  xkopt  21268  xkococnlem  21272  txcon  21302  qtopuni  21315  qtopkgen  21323  tgqtop  21325  regr1lem  21352  kqreglem1  21354  kqreglem2  21355  kqnrmlem1  21356  kqnrmlem2  21357  hmeoimaf1o  21383  reghmph  21406  nrmhmph  21407  filcon  21497  trfil1  21500  ufildr  21545  flimfil  21583  flimfnfcls  21642  alexsublem  21658  alexsubALTlem3  21663  ustbas2  21839  tgioo  22407  xrtgioo  22417  xrsmopn  22423  opnreen  22442  cnheibor  22562  cnllycmp  22563  lebnumlem1  22568  lebnumlem3  22570  bcthlem5  22933  bcth3  22936  voliunlem1  23125  voliunlem3  23127  volsup  23131  opnmbllem  23175  mbfimaopnlem  23228  lhop  23583  tglnpt  25244  tglineintmo  25337  ubthlem1  27110  shatomistici  28604  hatomistici  28605  unifi3  28873  tpr2rico  29286  hasheuni  29474  difelsiga  29523  prob01  29802  probdsb  29811  totprobd  29815  probmeasb  29819  cndprobtot  29825  orvcelval  29857  bnj1450  30372  bnj1501  30389  pconcon  30467  cvmsf1o  30508  cvmscld  30509  cvmsss2  30510  cvmopnlem  30514  cvmfolem  30515  cvmliftmolem1  30517  cvmliftlem6  30526  cvmliftlem8  30528  cvmlift2lem9  30547  cvmlift2lem11  30549  cvmlift2lem12  30550  cvmlift3lem6  30560  dfon2lem3  30934  dfon2lem7  30938  trpredpred  30972  frrlem11  31036  nobndlem2  31092  nobndlem8  31098  nofulllem3  31103  nofulllem5  31105  ntruni  31492  clsint2  31494  neibastop1  31524  topmeet  31529  topjoin  31530  fnemeet1  31531  fnejoin1  31533  opnmbllem0  32615  mbfresfi  32626  heiborlem1  32780  lssats  33317  dicval  35483  mapdunirnN  35957  isnacs3  36291  aomclem4  36645  kelac2  36653  ssuniint  38276  stoweidlem28  38921  stoweidlem50  38943  stoweidlem52  38945  stoweidlem53  38946  stoweidlem54  38947  prsal  39214  salincl  39219  saliincl  39221  saldifcl2  39222  salexct  39228  psmeasurelem  39363  caragenuni  39401  carageniuncl  39413  caratheodorylem1  39416  caratheodorylem2  39417  voncmpl  39511  setrec1lem2  42234  setrec2fun  42238