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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868

This theorem is used by:  unissel  4900  ssunieq  4904  pwuni  4906  pwel  5346  uniopel  5493  dmrnssfld  5958  unixp0  6281  elfvunirn  6909  sorpssuni  7734  iunpw  7771  pwuninel2  8273  pwuninel  8274  frrlem8  8293  frrlem10  8295  frrlem14  8299  fprresex  8310  onfununi  8331  tfrlem9  8375  tfrlem9a  8376  tfrlem13  8380  sbthlem1  9088  sbthlem2  9089  2pwuninel  9133  ordunifi  9263  unifpw  9325  fissuni  9327  unifi3  9332  dffi3  9404  cantnfp1lem3  9662  oemapvali  9666  cantnflem1  9671  cnfcom3lem  9685  rankuni2b  9838  carduni  9989  r0weon  10018  dfac8clem  10038  cardinfima  10103  alephfp  10114  iunfictbso  10120  dfac5lem4  10132  dfac2a  10135  dfacacn  10147  dfac12lem2  10150  kmlem2  10157  fin23lem16  10340  fin23lem21  10344  isf32lem5  10362  fin1a2lem11  10415  fin1a2lem13  10417  itunitc  10426  axdc2lem  10453  axdc3lem2  10456  ttukeylem5  10518  ttukeylem6  10519  fpwwe2lem10  10652  fpwwe2lem11  10653  fpwwe2lem12  10654  fpwwe2  10655  wunex2  10750  inatsk  10790  tskuni  10795  suplem1pr  11064  suplem2pr  11065  unirnioo  13505  mrcuni  17712  isacs3lem  18633  mrelatlub  18653  dprd2dlem1  20173  lbsextlem2  21349  eltopss  23135  toponss  23155  isbasis3g  23177  baspartn  23182  bastg  23194  tgcl  23197  fctop  23232  cctop  23234  ppttop  23235  epttop  23237  difopn  23262  ssntr  23286  isopn3  23294  isopn3i  23310  toponmre  23321  neiuni  23350  neiptoptop  23359  resttopon  23389  restopn2  23405  perfopn  23413  pnfnei  23448  mnfnei  23449  ssidcn  23483  lmcnp  23532  pnrmopn  23571  ist1-2  23575  nrmsep  23585  isnrm2  23586  isnrm3  23587  regsep2  23604  cncmp  23620  hauscmplem  23634  hauscmp  23635  conndisj  23644  cnconn  23650  conncompss  23661  islly2  23713  nllyrest  23715  nllyidm  23718  hausllycmp  23723  cldllycmp  23724  lly1stc  23725  comppfsc  23761  kgentopon  23767  kgenss  23772  llycmpkgen2  23779  1stckgen  23783  txuni2  23794  ptpjpre1  23800  ptuni2  23805  ptbasfi  23810  xkouni  23828  txcnpi  23837  ptpjopn  23841  txindis  23863  txnlly  23866  txtube  23869  hausdiag  23874  xkopt  23884  xkococnlem  23888  txconn  23918  qtopuni  23931  qtopkgen  23939  tgqtop  23941  regr1lem  23968  kqreglem1  23970  kqreglem2  23971  kqnrmlem1  23972  kqnrmlem2  23973  hmeoimaf1o  23999  reghmph  24022  nrmhmph  24023  filconn  24112  trfil1  24115  ufildr  24160  flimfil  24198  flimfnfcls  24257  alexsublem  24273  alexsubALTlem3  24278  ustbas2  24454  tgioo  25025  xrtgioo  25036  xrsmopn  25042  opnreen  25061  cnheibor  25186  cnllycmp  25187  lebnumlem1  25192  lebnumlem3  25194  bcthlem5  25559  bcth3  25562  voliunlem1  25781  voliunlem3  25783  volsup  25787  opnmbllem  25832  mbfimaopnlem  25886  lhop  26246  nosupno  27942  noinfno  27957  noetasuplem4  27975  noetainflem4  27979  tglnpt  28894  tglineintmo  28992  ubthlem1  31354  shatomistici  32845  hatomistici  32846  elrspunidl  33859  zarclsiin  34384  tpr2rico  34425  hasheuni  34598  prob01  34927  probdsb  34936  totprobd  34940  probmeasb  34944  cndprobtot  34950  orvcelval  34983  bnj1450  35562  bnj1501  35579  elwf  35607  pconnconn  35813  cvmsf1o  35854  cvmscld  35855  cvmsss2  35856  cvmopnlem  35860  cvmfolem  35861  cvmliftmolem1  35863  cvmliftlem6  35872  cvmliftlem8  35874  cvmlift2lem9  35893  cvmlift2lem11  35895  cvmlift2lem12  35896  cvmlift3lem6  35906  dfon2lem3  36365  dfon2lem7  36369  ntruni  36949  clsint2  36951  neibastop1  36981  topmeet  36986  topjoin  36987  fnemeet1  36988  fnejoin1  36990  dfttc2g  37128  opnmbllem0  38408  mbfresfi  38418  heiborlem1  38564  lssats  39888  dicval  42052  mapdunirnN  42526  isnacs3  43558  aomclem4  43901  kelac2  43909  onsupuni  44073  onsupmaxb  44083  mnuunid  45104  mnutrcld  45106  grumnudlem  45112  wfac8prim  45828  ssuniint  45915  stoweidlem28  46859  stoweidlem50  46881  stoweidlem52  46883  stoweidlem53  46884  stoweidlem54  46885  prsal  47149  salincl  47155  saliinclf  47157  saldifcl2  47159  salexct  47165  psmeasurelem  47301  caragenuni  47342  carageniuncl  47354  caratheodorylem1  47357  caratheodorylem2  47358  voncmpl  47452  opncldeqv  49831  opndisj  49832  unilbeu  49914  setrec1lem2  50617  setrec2fun  50621