Theorem elssuni 4899

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-uni 4868

This theorem is used by:  unissel  4900  ssunieq  4904  pwuni  4906  pwel  5343  uniopel  5489  dmrnssfld  5956  unixp0  6279  elfvunirn  6907  sorpssuni  7737  iunpw  7774  pwuninel2  8275  pwuninel  8276  frrlem8  8295  frrlem10  8297  frrlem14  8301  fprresex  8312  onfununi  8333  tfrlem9  8377  tfrlem9a  8378  tfrlem13  8382  sbthlem1  9090  sbthlem2  9091  2pwuninel  9135  ordunifi  9265  unifpw  9328  fissuni  9330  unifi3  9335  dffi3  9407  cantnfp1lem3  9665  oemapvali  9669  cantnflem1  9674  cnfcom3lem  9688  elwf  9823  rankuni2b  9848  setrec1lem2  9948  setrec2fun  9954  carduni  10043  r0weon  10072  dfac8clem  10092  cardinfima  10157  alephfp  10168  iunfictbso  10174  dfac5lem4  10186  dfac2a  10189  dfacacn  10201  dfac12lem2  10204  kmlem2  10211  fin23lem16  10394  fin23lem21  10398  isf32lem5  10416  fin1a2lem11  10469  fin1a2lem13  10471  itunitc  10480  axdc2lem  10507  axdc3lem2  10510  ttukeylem5  10572  ttukeylem6  10573  fpwwe2lem10  10706  fpwwe2lem11  10707  fpwwe2lem12  10708  fpwwe2  10709  wunex2  10804  inatsk  10844  tskuni  10849  suplem1pr  11118  suplem2pr  11119  unirnioo  13561  mrcuni  17775  isacs3lem  18696  mrelatlub  18716  dprd2dlem1  20237  lbsextlem2  21417  eltopss  23205  toponss  23225  isbasis3g  23247  baspartn  23252  bastg  23264  tgcl  23267  fctop  23302  cctop  23304  ppttop  23305  epttop  23307  difopn  23332  ssntr  23356  isopn3  23364  isopn3i  23380  toponmre  23391  neiuni  23420  neiptoptop  23429  resttopon  23459  restopn2  23475  perfopn  23483  pnfnei  23518  mnfnei  23519  ssidcn  23553  lmcnp  23602  pnrmopn  23641  ist1-2  23645  nrmsep  23655  isnrm2  23656  isnrm3  23657  regsep2  23674  cncmp  23690  hauscmplem  23704  hauscmp  23705  conndisj  23714  cnconn  23720  conncompss  23731  islly2  23783  nllyrest  23785  nllyidm  23788  hausllycmp  23793  cldllycmp  23794  lly1stc  23795  comppfsc  23831  kgentopon  23837  kgenss  23842  llycmpkgen2  23849  1stckgen  23853  txuni2  23864  ptpjpre1  23870  ptuni2  23875  ptbasfi  23880  xkouni  23898  txcnpi  23907  ptpjopn  23911  txindis  23933  txnlly  23936  txtube  23939  hausdiag  23944  xkopt  23954  xkococnlem  23958  txconn  23988  qtopuni  24001  qtopkgen  24009  tgqtop  24011  regr1lem  24038  kqreglem1  24040  kqreglem2  24041  kqnrmlem1  24042  kqnrmlem2  24043  hmeoimaf1o  24069  reghmph  24092  nrmhmph  24093  filconn  24182  trfil1  24185  ufildr  24230  flimfil  24268  flimfnfcls  24327  alexsublem  24343  alexsubALTlem3  24348  ustbas2  24524  tgioo  25095  xrtgioo  25106  xrsmopn  25112  opnreen  25131  cnheibor  25256  cnllycmp  25257  lebnumlem1  25262  lebnumlem3  25264  bcthlem5  25629  bcth3  25632  voliunlem1  25851  voliunlem3  25853  volsup  25857  opnmbllem  25902  mbfimaopnlem  25956  lhop  26316  nosupno  28042  noinfno  28057  noetasuplem4  28075  noetainflem4  28079  tglnpt  28994  tglineintmo  29092  ubthlem1  31454  shatomistici  32945  hatomistici  32946  elrspunidl  33960  zarclsiin  34485  tpr2rico  34526  hasheuni  34699  prob01  35028  probdsb  35037  totprobd  35041  probmeasb  35045  cndprobtot  35051  orvcelval  35084  bnj1450  35663  bnj1501  35680  pconnconn  35965  cvmsf1o  36006  cvmscld  36007  cvmsss2  36008  cvmopnlem  36012  cvmfolem  36013  cvmliftmolem1  36015  cvmliftlem6  36024  cvmliftlem8  36026  cvmlift2lem9  36045  cvmlift2lem11  36047  cvmlift2lem12  36048  cvmlift3lem6  36058  dfon2lem3  36517  dfon2lem7  36521  ntruni  37085  clsint2  37087  neibastop1  37117  topmeet  37122  topjoin  37123  fnemeet1  37124  fnejoin1  37126  dfttc2g  37264  opnmbllem0  38542  mbfresfi  38552  heiborlem1  38713  lssats  40037  dicval  42201  mapdunirnN  42675  isnacs3  43674  aomclem4  44017  kelac2  44025  onsupuni  44189  onsupmaxb  44199  mnuunid  45220  mnutrcld  45222  grumnudlem  45228  wfac8prim  45944  ssuniint  46038  stoweidlem28  46982  stoweidlem50  47004  stoweidlem52  47006  stoweidlem53  47007  stoweidlem54  47008  prsal  47272  salincl  47278  saliinclf  47280  saldifcl2  47282  salexct  47288  psmeasurelem  47424  caragenuni  47465  carageniuncl  47477  caratheodorylem1  47480  caratheodorylem2  47481  voncmpl  47575  opncldbid  49954  opndisj  49955  unilbeu  50037