Theorem elssuni 4894

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3901  ∪ cuni 4863

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-uni 4864

This theorem is referenced by:  unissel  4895  ssunieq  4899  pwuni  4901  pwel  5326  uniopel  5464  dmrnssfld  5923  unixp0  6241  elfvunirn  6864  sorpssuni  7677  iunpw  7716  pwuninel2  8216  frrlem8  8235  frrlem10  8237  frrlem14  8241  fprresex  8252  onfununi  8273  tfrlem9  8316  tfrlem9a  8317  tfrlem13  8321  sbthlem1  9015  sbthlem2  9016  2pwuninel  9060  ordunifi  9190  unifpw  9255  fissuni  9257  unifi3  9262  dffi3  9334  cantnfp1lem3  9589  oemapvali  9593  cantnflem1  9598  cnfcom3lem  9612  rankuni2b  9765  carduni  9893  r0weon  9922  dfac8clem  9942  cardinfima  10007  alephfp  10018  iunfictbso  10024  dfac5lem4  10036  dfac5lem4OLD  10038  dfac2a  10040  dfacacn  10052  dfac12lem2  10055  kmlem2  10062  fin23lem16  10245  fin23lem21  10249  isf32lem5  10267  fin1a2lem11  10320  fin1a2lem13  10322  itunitc  10331  axdc2lem  10358  axdc3lem2  10361  ttukeylem5  10423  ttukeylem6  10424  fpwwe2lem10  10551  fpwwe2lem11  10552  fpwwe2lem12  10553  fpwwe2  10554  wunex2  10649  inatsk  10689  tskuni  10694  suplem1pr  10963  suplem2pr  10964  unirnioo  13365  mrcuni  17544  isacs3lem  18465  mrelatlub  18485  dprd2dlem1  19972  lbsextlem2  21114  eltopss  22851  toponss  22871  isbasis3g  22893  baspartn  22898  bastg  22910  tgcl  22913  fctop  22948  cctop  22950  ppttop  22951  epttop  22953  difopn  22978  ssntr  23002  isopn3  23010  isopn3i  23026  toponmre  23037  neiuni  23066  neiptoptop  23075  resttopon  23105  restopn2  23121  perfopn  23129  pnfnei  23164  mnfnei  23165  ssidcn  23199  lmcnp  23248  pnrmopn  23287  ist1-2  23291  nrmsep  23301  isnrm2  23302  isnrm3  23303  regsep2  23320  cncmp  23336  hauscmplem  23350  hauscmp  23351  conndisj  23360  cnconn  23366  conncompss  23377  islly2  23428  nllyrest  23430  nllyidm  23433  hausllycmp  23438  cldllycmp  23439  lly1stc  23440  comppfsc  23476  kgentopon  23482  kgenss  23487  llycmpkgen2  23494  1stckgen  23498  txuni2  23509  ptpjpre1  23515  ptuni2  23520  ptbasfi  23525  xkouni  23543  txcnpi  23552  ptpjopn  23556  txindis  23578  txnlly  23581  txtube  23584  hausdiag  23589  xkopt  23599  xkococnlem  23603  txconn  23633  qtopuni  23646  qtopkgen  23654  tgqtop  23656  regr1lem  23683  kqreglem1  23685  kqreglem2  23686  kqnrmlem1  23687  kqnrmlem2  23688  hmeoimaf1o  23714  reghmph  23737  nrmhmph  23738  filconn  23827  trfil1  23830  ufildr  23875  flimfil  23913  flimfnfcls  23972  alexsublem  23988  alexsubALTlem3  23993  ustbas2  24169  tgioo  24740  xrtgioo  24751  xrsmopn  24757  opnreen  24776  cnheibor  24910  cnllycmp  24911  lebnumlem1  24916  lebnumlem3  24918  bcthlem5  25284  bcth3  25287  voliunlem1  25507  voliunlem3  25509  volsup  25513  opnmbllem  25558  mbfimaopnlem  25612  lhop  25977  nosupno  27671  noinfno  27686  noetasuplem4  27704  noetainflem4  27708  tglnpt  28621  tglineintmo  28714  ubthlem1  30945  shatomistici  32436  hatomistici  32437  elrspunidl  33509  zarclsiin  34028  tpr2rico  34069  hasheuni  34242  difelsiga  34290  prob01  34570  probdsb  34579  totprobd  34583  probmeasb  34587  cndprobtot  34593  orvcelval  34626  bnj1450  35206  bnj1501  35223  elwf  35253  pconnconn  35425  cvmsf1o  35466  cvmscld  35467  cvmsss2  35468  cvmopnlem  35472  cvmfolem  35473  cvmliftmolem1  35475  cvmliftlem6  35484  cvmliftlem8  35486  cvmlift2lem9  35505  cvmlift2lem11  35507  cvmlift2lem12  35508  cvmlift3lem6  35518  dfon2lem3  35977  dfon2lem7  35981  ntruni  36521  clsint2  36523  neibastop1  36553  topmeet  36558  topjoin  36559  fnemeet1  36560  fnejoin1  36562  opnmbllem0  37853  mbfresfi  37863  heiborlem1  38008  lssats  39268  dicval  41432  mapdunirnN  41906  isnacs3  42948  aomclem4  43295  kelac2  43303  onsupuni  43467  onsupmaxb  43477  mnuunid  44514  mnutrcld  44516  grumnudlem  44522  wfac8prim  45239  ssuniint  45319  stoweidlem28  46268  stoweidlem50  46290  stoweidlem52  46292  stoweidlem53  46293  stoweidlem54  46294  prsal  46558  salincl  46564  saliinclf  46566  saldifcl2  46568  salexct  46574  psmeasurelem  46710  caragenuni  46751  carageniuncl  46763  caratheodorylem1  46766  caratheodorylem2  46767  voncmpl  46861  opncldeqv  49143  opndisj  49144  unilbeu  49226  setrec1lem2  49929  setrec2fun  49933