Theorem elssuni 4902

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900  ∪ cuni 4870

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871

This theorem is used by:  unissel  4903  ssunieq  4907  pwuni  4909  pwel  5347  uniopel  5493  dmrnssfld  5963  unixp0  6304  elfvunirn  6938  sorpssuni  7772  iunpw  7809  pwuninel2  8319  pwuninel  8320  frrlem8  8339  frrlem10  8341  frrlem14  8345  fprresex  8356  onfununi  8377  tfrlem9  8421  tfrlem9a  8422  tfrlem13  8426  sbthlem1  9134  sbthlem2  9135  2pwuninel  9179  ordunifi  9309  unifpw  9372  fissuni  9374  unifi3  9379  dffi3  9450  cantnfp1lem3  9708  oemapvali  9712  cantnflem1  9717  cnfcom3lem  9731  elwf  9869  rankuni2b  9894  setrec1lem2  9994  setrec2fun  10000  carduni  10089  r0weon  10118  dfac8clem  10138  cardinfima  10203  alephfp  10214  iunfictbso  10220  dfac5lem4  10232  dfac2a  10235  dfacacn  10247  dfac12lem2  10250  kmlem2  10257  fin23lem16  10440  fin23lem21  10444  isf32lem5  10462  fin1a2lem11  10515  fin1a2lem13  10517  itunitc  10526  axdc2lem  10553  axdc3lem2  10556  ttukeylem5  10618  ttukeylem6  10619  fpwwe2lem10  10752  fpwwe2lem11  10753  fpwwe2lem12  10754  fpwwe2  10755  wunex2  10850  inatsk  10890  tskuni  10895  suplem1pr  11164  suplem2pr  11165  unirnioo  13607  mrcuni  17824  isacs3lem  18745  mrelatlub  18765  dprd2dlem1  20287  lbsextlem2  21467  eltopss  23255  toponss  23275  isbasis3g  23297  baspartn  23302  bastg  23314  tgcl  23317  fctop  23352  cctop  23354  ppttop  23355  epttop  23357  difopn  23382  ssntr  23406  isopn3  23414  isopn3i  23430  toponmre  23441  neiuni  23470  neiptoptop  23479  resttopon  23509  restopn2  23525  perfopn  23533  pnfnei  23568  mnfnei  23569  ssidcn  23603  lmcnp  23652  pnrmopn  23691  ist1-2  23695  nrmsep  23705  isnrm2  23706  isnrm3  23707  regsep2  23724  cncmp  23740  hauscmplem  23754  hauscmp  23755  conndisj  23764  cnconn  23770  conncompss  23781  islly2  23833  nllyrest  23835  nllyidm  23838  hausllycmp  23843  cldllycmp  23844  lly1stc  23845  comppfsc  23881  kgentopon  23887  kgenss  23892  llycmpkgen2  23899  1stckgen  23903  txuni2  23914  ptpjpre1  23920  ptuni2  23925  ptbasfi  23930  xkouni  23948  txcnpi  23957  ptpjopn  23961  txindis  23983  txnlly  23986  txtube  23989  hausdiag  23994  xkopt  24004  xkococnlem  24008  txconn  24038  qtopuni  24051  qtopkgen  24059  tgqtop  24061  regr1lem  24088  kqreglem1  24090  kqreglem2  24091  kqnrmlem1  24092  kqnrmlem2  24093  hmeoimaf1o  24119  reghmph  24142  nrmhmph  24143  filconn  24232  trfil1  24235  ufildr  24280  flimfil  24318  flimfnfcls  24377  alexsublem  24393  alexsubALTlem3  24398  ustbas2  24574  tgioo  25145  xrtgioo  25156  xrsmopn  25162  opnreen  25181  cnheibor  25306  cnllycmp  25307  lebnumlem1  25312  lebnumlem3  25314  bcthlem5  25679  bcth3  25682  voliunlem1  25901  voliunlem3  25903  volsup  25907  opnmbllem  25952  mbfimaopnlem  26006  lhop  26366  nosupno  28090  noinfno  28105  noetasuplem4  28123  noetainflem4  28127  tglnpt  29042  tglineintmo  29140  ubthlem1  31502  shatomistici  32993  hatomistici  32994  elrspunidl  34048  zarclsiin  34573  tpr2rico  34614  hasheuni  34787  prob01  35115  probdsb  35124  totprobd  35128  probmeasb  35132  cndprobtot  35138  orvcelval  35171  bnj1450  35750  bnj1501  35767  pconnconn  36163  cvmsf1o  36204  cvmscld  36205  cvmsss2  36206  cvmopnlem  36210  cvmfolem  36211  cvmliftmolem1  36213  cvmliftlem6  36222  cvmliftlem8  36224  cvmlift2lem9  36243  cvmlift2lem11  36245  cvmlift2lem12  36246  cvmlift3lem6  36256  cardprcr  36633  dfon2lem3  36725  dfon2lem7  36729  ntruni  37293  clsint2  37295  neibastop1  37325  topmeet  37330  topjoin  37331  fnemeet1  37332  fnejoin1  37334  dfttc2g  37472  opnmbllem0  38766  mbfresfi  38776  heiborlem1  38937  lssats  40261  dicval  42425  mapdunirnN  42899  isnacs3  43914  aomclem4  44252  kelac2  44260  onsupuni  44423  onsupmaxb  44433  mnuunid  45453  mnutrcld  45455  grumnudlem  45461  wfac8prim  46187  ssuniint  46300  stoweidlem28  47243  stoweidlem50  47265  stoweidlem52  47267  stoweidlem53  47268  stoweidlem54  47269  prsal  47533  salincl  47539  saliinclf  47541  saldifcl2  47543  salexct  47549  psmeasurelem  47685  caragenuni  47726  carageniuncl  47738  caratheodorylem1  47741  caratheodorylem2  47742  voncmpl  47836  opncldbid  50221  opndisj  50222  unilbeu  50304