Theorem elssuni 4830

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3881  ∪ cuni 4800

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801

This theorem is referenced by:  unissel  4831  ssunieq  4835  pwuni  4837  pwel  5247  uniopel  5371  dmrnssfld  5806  unixp0  6102  fvssunirn  6674  sorpssuni  7438  iunpw  7473  pwuninel2  7923  wfrlem12  7949  wfrlem16  7953  wfrlem17  7954  onfununi  7961  tfrlem9  8004  tfrlem9a  8005  tfrlem13  8009  sbthlem1  8611  sbthlem2  8612  2pwuninel  8656  ordunifi  8752  unifpw  8811  fissuni  8813  dffi3  8879  cantnfp1lem3  9127  oemapvali  9131  cantnflem1  9136  cnfcom3lem  9150  rankuni2b  9266  carduni  9394  r0weon  9423  dfac8clem  9443  cardinfima  9508  alephfp  9519  iunfictbso  9525  dfac5lem4  9537  dfac2a  9540  dfacacn  9552  dfac12lem2  9555  kmlem2  9562  fin23lem16  9746  fin23lem21  9750  isf32lem5  9768  fin1a2lem11  9821  fin1a2lem13  9823  itunitc  9832  axdc2lem  9859  axdc3lem2  9862  ttukeylem5  9924  ttukeylem6  9925  fpwwe2lem11  10051  fpwwe2lem12  10052  fpwwe2lem13  10053  fpwwe2  10054  wunex2  10149  inatsk  10189  tskuni  10194  suplem1pr  10463  suplem2pr  10464  unirnioo  12827  mrcuni  16884  isacs3lem  17768  mrelatlub  17788  dprd2dlem1  19156  lbsextlem2  19924  eltopss  21512  toponss  21532  isbasis3g  21554  baspartn  21559  bastg  21571  tgcl  21574  fctop  21609  cctop  21611  ppttop  21612  epttop  21614  difopn  21639  ssntr  21663  isopn3  21671  isopn3i  21687  toponmre  21698  neiuni  21727  neiptoptop  21736  resttopon  21766  restopn2  21782  perfopn  21790  pnfnei  21825  mnfnei  21826  ssidcn  21860  lmcnp  21909  pnrmopn  21948  ist1-2  21952  nrmsep  21962  isnrm2  21963  isnrm3  21964  regsep2  21981  cncmp  21997  hauscmplem  22011  hauscmp  22012  conndisj  22021  cnconn  22027  conncompss  22038  islly2  22089  nllyrest  22091  nllyidm  22094  hausllycmp  22099  cldllycmp  22100  lly1stc  22101  comppfsc  22137  kgentopon  22143  kgenss  22148  llycmpkgen2  22155  1stckgen  22159  txuni2  22170  ptpjpre1  22176  ptuni2  22181  ptbasfi  22186  xkouni  22204  txcnpi  22213  ptpjopn  22217  txindis  22239  txnlly  22242  txtube  22245  hausdiag  22250  xkopt  22260  xkococnlem  22264  txconn  22294  qtopuni  22307  qtopkgen  22315  tgqtop  22317  regr1lem  22344  kqreglem1  22346  kqreglem2  22347  kqnrmlem1  22348  kqnrmlem2  22349  hmeoimaf1o  22375  reghmph  22398  nrmhmph  22399  filconn  22488  trfil1  22491  ufildr  22536  flimfil  22574  flimfnfcls  22633  alexsublem  22649  alexsubALTlem3  22654  ustbas2  22831  tgioo  23401  xrtgioo  23411  xrsmopn  23417  opnreen  23436  cnheibor  23560  cnllycmp  23561  lebnumlem1  23566  lebnumlem3  23568  bcthlem5  23932  bcth3  23935  voliunlem1  24154  voliunlem3  24156  volsup  24160  opnmbllem  24205  mbfimaopnlem  24259  lhop  24619  tglnpt  26343  tglineintmo  26436  ubthlem1  28653  shatomistici  30144  hatomistici  30145  unifi3  30474  elrspunidl  31014  zarclsiin  31224  tpr2rico  31265  hasheuni  31454  difelsiga  31502  prob01  31781  probdsb  31790  totprobd  31794  probmeasb  31798  cndprobtot  31804  orvcelval  31836  bnj1450  32432  bnj1501  32449  pconnconn  32591  cvmsf1o  32632  cvmscld  32633  cvmsss2  32634  cvmopnlem  32638  cvmfolem  32639  cvmliftmolem1  32641  cvmliftlem6  32650  cvmliftlem8  32652  cvmlift2lem9  32671  cvmlift2lem11  32673  cvmlift2lem12  32674  cvmlift3lem6  32684  dfon2lem3  33143  dfon2lem7  33147  trpredpred  33180  frrlem8  33243  frrlem10  33245  frrlem14  33249  nosupno  33316  nosupbday  33318  noetalem3  33332  ntruni  33788  clsint2  33790  neibastop1  33820  topmeet  33825  topjoin  33826  fnemeet1  33827  fnejoin1  33829  opnmbllem0  35093  mbfresfi  35103  heiborlem1  35249  lssats  36308  dicval  38472  mapdunirnN  38946  isnacs3  39651  aomclem4  40001  kelac2  40009  mnuunid  40985  mnutrcld  40987  grumnudlem  40993  ssuniint  41714  stoweidlem28  42670  stoweidlem50  42692  stoweidlem52  42694  stoweidlem53  42695  stoweidlem54  42696  prsal  42960  salincl  42965  saliincl  42967  saldifcl2  42968  salexct  42974  psmeasurelem  43109  caragenuni  43150  carageniuncl  43162  caratheodorylem1  43165  caratheodorylem2  43166  voncmpl  43260  setrec1lem2  45218  setrec2fun  45222