Theorem elssuni 4909

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3908  ∪ cuni 4877

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-uni 4878

This theorem is used by:  unissel  4910  ssunieq  4914  pwuni  4916  pwel  5357  uniopel  5504  dmrnssfld  5969  unixp0  6291  elfvunirn  6918  sorpssuni  7742  iunpw  7779  pwuninel2  8279  pwuninel  8280  frrlem8  8299  frrlem10  8301  frrlem14  8305  fprresex  8316  onfununi  8337  tfrlem9  8381  tfrlem9a  8382  tfrlem13  8386  sbthlem1  9085  sbthlem2  9086  2pwuninel  9130  ordunifi  9260  unifpw  9322  fissuni  9324  unifi3  9329  dffi3  9401  cantnfp1lem3  9659  oemapvali  9663  cantnflem1  9668  cnfcom3lem  9682  rankuni2b  9835  carduni  9986  r0weon  10015  dfac8clem  10035  cardinfima  10100  alephfp  10111  iunfictbso  10117  dfac5lem4  10129  dfac2a  10132  dfacacn  10144  dfac12lem2  10147  kmlem2  10154  fin23lem16  10337  fin23lem21  10341  isf32lem5  10359  fin1a2lem11  10412  fin1a2lem13  10414  itunitc  10423  axdc2lem  10450  axdc3lem2  10453  ttukeylem5  10515  ttukeylem6  10516  fpwwe2lem10  10643  fpwwe2lem11  10644  fpwwe2lem12  10645  fpwwe2  10646  wunex2  10741  inatsk  10781  tskuni  10786  suplem1pr  11055  suplem2pr  11056  unirnioo  13494  mrcuni  17702  isacs3lem  18623  mrelatlub  18643  dprd2dlem1  20144  lbsextlem2  21320  eltopss  23101  toponss  23121  isbasis3g  23143  baspartn  23148  bastg  23160  tgcl  23163  fctop  23198  cctop  23200  ppttop  23201  epttop  23203  difopn  23228  ssntr  23252  isopn3  23260  isopn3i  23276  toponmre  23287  neiuni  23316  neiptoptop  23325  resttopon  23355  restopn2  23371  perfopn  23379  pnfnei  23414  mnfnei  23415  ssidcn  23449  lmcnp  23498  pnrmopn  23537  ist1-2  23541  nrmsep  23551  isnrm2  23552  isnrm3  23553  regsep2  23570  cncmp  23586  hauscmplem  23600  hauscmp  23601  conndisj  23610  cnconn  23616  conncompss  23627  islly2  23678  nllyrest  23680  nllyidm  23683  hausllycmp  23688  cldllycmp  23689  lly1stc  23690  comppfsc  23726  kgentopon  23732  kgenss  23737  llycmpkgen2  23744  1stckgen  23748  txuni2  23759  ptpjpre1  23765  ptuni2  23770  ptbasfi  23775  xkouni  23793  txcnpi  23802  ptpjopn  23806  txindis  23828  txnlly  23831  txtube  23834  hausdiag  23839  xkopt  23849  xkococnlem  23853  txconn  23883  qtopuni  23896  qtopkgen  23904  tgqtop  23906  regr1lem  23933  kqreglem1  23935  kqreglem2  23936  kqnrmlem1  23937  kqnrmlem2  23938  hmeoimaf1o  23964  reghmph  23987  nrmhmph  23988  filconn  24077  trfil1  24080  ufildr  24125  flimfil  24163  flimfnfcls  24222  alexsublem  24238  alexsubALTlem3  24243  ustbas2  24419  tgioo  24990  xrtgioo  25001  xrsmopn  25007  opnreen  25026  cnheibor  25151  cnllycmp  25152  lebnumlem1  25157  lebnumlem3  25159  bcthlem5  25524  bcth3  25527  voliunlem1  25746  voliunlem3  25748  volsup  25752  opnmbllem  25797  mbfimaopnlem  25851  lhop  26212  nosupno  27904  noinfno  27919  noetasuplem4  27937  noetainflem4  27941  tglnpt  28855  tglineintmo  28952  ubthlem1  31259  shatomistici  32750  hatomistici  32751  elrspunidl  33767  zarclsiin  34292  tpr2rico  34333  hasheuni  34506  prob01  34835  probdsb  34844  totprobd  34848  probmeasb  34852  cndprobtot  34858  orvcelval  34891  bnj1450  35470  bnj1501  35487  elwf  35515  pconnconn  35744  cvmsf1o  35785  cvmscld  35786  cvmsss2  35787  cvmopnlem  35791  cvmfolem  35792  cvmliftmolem1  35794  cvmliftlem6  35803  cvmliftlem8  35805  cvmlift2lem9  35824  cvmlift2lem11  35826  cvmlift2lem12  35827  cvmlift3lem6  35837  dfon2lem3  36296  dfon2lem7  36300  ntruni  36879  clsint2  36881  neibastop1  36911  topmeet  36916  topjoin  36917  fnemeet1  36918  fnejoin1  36920  dfttc2g  37058  opnmbllem0  38348  mbfresfi  38358  heiborlem1  38503  lssats  39827  dicval  41991  mapdunirnN  42465  isnacs3  43482  aomclem4  43825  kelac2  43833  onsupuni  43997  onsupmaxb  44007  mnuunid  45028  mnutrcld  45030  grumnudlem  45036  wfac8prim  45752  ssuniint  45839  stoweidlem28  46783  stoweidlem50  46805  stoweidlem52  46807  stoweidlem53  46808  stoweidlem54  46809  prsal  47073  salincl  47079  saliinclf  47081  saldifcl2  47083  salexct  47089  psmeasurelem  47225  caragenuni  47266  carageniuncl  47278  caratheodorylem1  47281  caratheodorylem2  47282  voncmpl  47376  opncldeqv  49721  opndisj  49722  unilbeu  49804  setrec1lem2  50507  setrec2fun  50511