Theorem elssuni 4881

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3889  ∪ cuni 4850

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-uni 4851

This theorem is referenced by:  unissel  4882  ssunieq  4886  pwuni  4888  pwel  5323  uniopel  5470  dmrnssfld  5929  unixp0  6247  elfvunirn  6870  sorpssuni  7686  iunpw  7725  pwuninel2  8224  frrlem8  8243  frrlem10  8245  frrlem14  8249  fprresex  8260  onfununi  8281  tfrlem9  8324  tfrlem9a  8325  tfrlem13  8329  sbthlem1  9025  sbthlem2  9026  2pwuninel  9070  ordunifi  9200  unifpw  9265  fissuni  9267  unifi3  9272  dffi3  9344  cantnfp1lem3  9601  oemapvali  9605  cantnflem1  9610  cnfcom3lem  9624  rankuni2b  9777  carduni  9905  r0weon  9934  dfac8clem  9954  cardinfima  10019  alephfp  10030  iunfictbso  10036  dfac5lem4  10048  dfac5lem4OLD  10050  dfac2a  10052  dfacacn  10064  dfac12lem2  10067  kmlem2  10074  fin23lem16  10257  fin23lem21  10261  isf32lem5  10279  fin1a2lem11  10332  fin1a2lem13  10334  itunitc  10343  axdc2lem  10370  axdc3lem2  10373  ttukeylem5  10435  ttukeylem6  10436  fpwwe2lem10  10563  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  wunex2  10661  inatsk  10701  tskuni  10706  suplem1pr  10975  suplem2pr  10976  unirnioo  13402  mrcuni  17587  isacs3lem  18508  mrelatlub  18528  dprd2dlem1  20018  lbsextlem2  21157  eltopss  22872  toponss  22892  isbasis3g  22914  baspartn  22919  bastg  22931  tgcl  22934  fctop  22969  cctop  22971  ppttop  22972  epttop  22974  difopn  22999  ssntr  23023  isopn3  23031  isopn3i  23047  toponmre  23058  neiuni  23087  neiptoptop  23096  resttopon  23126  restopn2  23142  perfopn  23150  pnfnei  23185  mnfnei  23186  ssidcn  23220  lmcnp  23269  pnrmopn  23308  ist1-2  23312  nrmsep  23322  isnrm2  23323  isnrm3  23324  regsep2  23341  cncmp  23357  hauscmplem  23371  hauscmp  23372  conndisj  23381  cnconn  23387  conncompss  23398  islly2  23449  nllyrest  23451  nllyidm  23454  hausllycmp  23459  cldllycmp  23460  lly1stc  23461  comppfsc  23497  kgentopon  23503  kgenss  23508  llycmpkgen2  23515  1stckgen  23519  txuni2  23530  ptpjpre1  23536  ptuni2  23541  ptbasfi  23546  xkouni  23564  txcnpi  23573  ptpjopn  23577  txindis  23599  txnlly  23602  txtube  23605  hausdiag  23610  xkopt  23620  xkococnlem  23624  txconn  23654  qtopuni  23667  qtopkgen  23675  tgqtop  23677  regr1lem  23704  kqreglem1  23706  kqreglem2  23707  kqnrmlem1  23708  kqnrmlem2  23709  hmeoimaf1o  23735  reghmph  23758  nrmhmph  23759  filconn  23848  trfil1  23851  ufildr  23896  flimfil  23934  flimfnfcls  23993  alexsublem  24009  alexsubALTlem3  24014  ustbas2  24190  tgioo  24761  xrtgioo  24772  xrsmopn  24778  opnreen  24797  cnheibor  24922  cnllycmp  24923  lebnumlem1  24928  lebnumlem3  24930  bcthlem5  25295  bcth3  25298  voliunlem1  25517  voliunlem3  25519  volsup  25523  opnmbllem  25568  mbfimaopnlem  25622  lhop  25983  nosupno  27667  noinfno  27682  noetasuplem4  27700  noetainflem4  27704  tglnpt  28617  tglineintmo  28710  ubthlem1  30941  shatomistici  32432  hatomistici  32433  elrspunidl  33488  zarclsiin  34015  tpr2rico  34056  hasheuni  34229  difelsiga  34277  prob01  34557  probdsb  34566  totprobd  34570  probmeasb  34574  cndprobtot  34580  orvcelval  34613  bnj1450  35192  bnj1501  35209  elwf  35240  pconnconn  35413  cvmsf1o  35454  cvmscld  35455  cvmsss2  35456  cvmopnlem  35460  cvmfolem  35461  cvmliftmolem1  35463  cvmliftlem6  35472  cvmliftlem8  35474  cvmlift2lem9  35493  cvmlift2lem11  35495  cvmlift2lem12  35496  cvmlift3lem6  35506  dfon2lem3  35965  dfon2lem7  35969  ntruni  36509  clsint2  36511  neibastop1  36541  topmeet  36546  topjoin  36547  fnemeet1  36548  fnejoin1  36550  dfttc2g  36688  opnmbllem0  37977  mbfresfi  37987  heiborlem1  38132  lssats  39458  dicval  41622  mapdunirnN  42096  isnacs3  43142  aomclem4  43485  kelac2  43493  onsupuni  43657  onsupmaxb  43667  mnuunid  44704  mnutrcld  44706  grumnudlem  44712  wfac8prim  45429  ssuniint  45509  stoweidlem28  46456  stoweidlem50  46478  stoweidlem52  46480  stoweidlem53  46481  stoweidlem54  46482  prsal  46746  salincl  46752  saliinclf  46754  saldifcl2  46756  salexct  46762  psmeasurelem  46898  caragenuni  46939  carageniuncl  46951  caratheodorylem1  46954  caratheodorylem2  46955  voncmpl  47049  opncldeqv  49377  opndisj  49378  unilbeu  49460  setrec1lem2  50163  setrec2fun  50167