Theorem elssuni 4940

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

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3947  ∪ cuni 4907

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-uni 4908

This theorem is referenced by:  unissel  4941  ssunieq  4946  pwuni  4948  pwel  5378  uniopel  5515  dmrnssfld  5967  unixp0  6279  elfvunirn  6920  fvssunirnOLD  6922  sorpssuni  7718  iunpw  7754  pwuninel2  8255  frrlem8  8274  frrlem10  8276  frrlem14  8280  fprresex  8291  wfrlem12OLD  8316  wfrlem16OLD  8320  wfrlem17OLD  8321  onfununi  8337  tfrlem9  8381  tfrlem9a  8382  tfrlem13  8386  sbthlem1  9079  sbthlem2  9080  2pwuninel  9128  ordunifi  9289  unifpw  9351  fissuni  9353  dffi3  9422  cantnfp1lem3  9671  oemapvali  9675  cantnflem1  9680  cnfcom3lem  9694  rankuni2b  9844  carduni  9972  r0weon  10003  dfac8clem  10023  cardinfima  10088  alephfp  10099  iunfictbso  10105  dfac5lem4  10117  dfac2a  10120  dfacacn  10132  dfac12lem2  10135  kmlem2  10142  fin23lem16  10326  fin23lem21  10330  isf32lem5  10348  fin1a2lem11  10401  fin1a2lem13  10403  itunitc  10412  axdc2lem  10439  axdc3lem2  10442  ttukeylem5  10504  ttukeylem6  10505  fpwwe2lem10  10631  fpwwe2lem11  10632  fpwwe2lem12  10633  fpwwe2  10634  wunex2  10729  inatsk  10769  tskuni  10774  suplem1pr  11043  suplem2pr  11044  unirnioo  13422  mrcuni  17561  isacs3lem  18491  mrelatlub  18511  dprd2dlem1  19905  lbsextlem2  20764  eltopss  22400  toponss  22420  isbasis3g  22443  baspartn  22448  bastg  22460  tgcl  22463  fctop  22498  cctop  22500  ppttop  22501  epttop  22503  difopn  22529  ssntr  22553  isopn3  22561  isopn3i  22577  toponmre  22588  neiuni  22617  neiptoptop  22626  resttopon  22656  restopn2  22672  perfopn  22680  pnfnei  22715  mnfnei  22716  ssidcn  22750  lmcnp  22799  pnrmopn  22838  ist1-2  22842  nrmsep  22852  isnrm2  22853  isnrm3  22854  regsep2  22871  cncmp  22887  hauscmplem  22901  hauscmp  22902  conndisj  22911  cnconn  22917  conncompss  22928  islly2  22979  nllyrest  22981  nllyidm  22984  hausllycmp  22989  cldllycmp  22990  lly1stc  22991  comppfsc  23027  kgentopon  23033  kgenss  23038  llycmpkgen2  23045  1stckgen  23049  txuni2  23060  ptpjpre1  23066  ptuni2  23071  ptbasfi  23076  xkouni  23094  txcnpi  23103  ptpjopn  23107  txindis  23129  txnlly  23132  txtube  23135  hausdiag  23140  xkopt  23150  xkococnlem  23154  txconn  23184  qtopuni  23197  qtopkgen  23205  tgqtop  23207  regr1lem  23234  kqreglem1  23236  kqreglem2  23237  kqnrmlem1  23238  kqnrmlem2  23239  hmeoimaf1o  23265  reghmph  23288  nrmhmph  23289  filconn  23378  trfil1  23381  ufildr  23426  flimfil  23464  flimfnfcls  23523  alexsublem  23539  alexsubALTlem3  23544  ustbas2  23721  tgioo  24303  xrtgioo  24313  xrsmopn  24319  opnreen  24338  cnheibor  24462  cnllycmp  24463  lebnumlem1  24468  lebnumlem3  24470  bcthlem5  24836  bcth3  24839  voliunlem1  25058  voliunlem3  25060  volsup  25064  opnmbllem  25109  mbfimaopnlem  25163  lhop  25524  nosupno  27195  noinfno  27210  noetasuplem4  27228  noetainflem4  27232  tglnpt  27789  tglineintmo  27882  ubthlem1  30110  shatomistici  31601  hatomistici  31602  unifi3  31924  elrspunidl  32534  zarclsiin  32839  tpr2rico  32880  hasheuni  33071  difelsiga  33119  prob01  33400  probdsb  33409  totprobd  33413  probmeasb  33417  cndprobtot  33423  orvcelval  33455  bnj1450  34049  bnj1501  34066  pconnconn  34210  cvmsf1o  34251  cvmscld  34252  cvmsss2  34253  cvmopnlem  34257  cvmfolem  34258  cvmliftmolem1  34260  cvmliftlem6  34269  cvmliftlem8  34271  cvmlift2lem9  34290  cvmlift2lem11  34292  cvmlift2lem12  34293  cvmlift3lem6  34303  dfon2lem3  34745  dfon2lem7  34749  ntruni  35200  clsint2  35202  neibastop1  35232  topmeet  35237  topjoin  35238  fnemeet1  35239  fnejoin1  35241  opnmbllem0  36512  mbfresfi  36522  heiborlem1  36667  lssats  37870  dicval  40035  mapdunirnN  40509  isnacs3  41433  aomclem4  41784  kelac2  41792  onsupuni  41963  onsupmaxb  41973  mnuunid  43021  mnutrcld  43023  grumnudlem  43029  ssuniint  43752  stoweidlem28  44730  stoweidlem50  44752  stoweidlem52  44754  stoweidlem53  44755  stoweidlem54  44756  prsal  45020  salincl  45026  saliinclf  45028  saldifcl2  45030  salexct  45036  psmeasurelem  45172  caragenuni  45213  carageniuncl  45225  caratheodorylem1  45228  caratheodorylem2  45229  voncmpl  45323  opncldeqv  47487  opndisj  47488  unilbeu  47563  setrec1lem2  47686  setrec2fun  47690