Theorem elssuni 4898

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3895  ∪ cuni 4866

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867

This theorem is used by:  unissel  4899  ssunieq  4903  pwuni  4905  pwel  5342  uniopel  5488  dmrnssfld  5955  unixp0  6286  elfvunirn  6915  sorpssuni  7748  iunpw  7785  pwuninel2  8294  pwuninel  8295  frrlem8  8314  frrlem10  8316  frrlem14  8320  fprresex  8331  onfununi  8352  tfrlem9  8396  tfrlem9a  8397  tfrlem13  8401  sbthlem1  9109  sbthlem2  9110  2pwuninel  9154  ordunifi  9284  unifpw  9347  fissuni  9349  unifi3  9354  dffi3  9426  cantnfp1lem3  9684  oemapvali  9688  cantnflem1  9693  cnfcom3lem  9707  elwf  9845  rankuni2b  9870  setrec1lem2  9970  setrec2fun  9976  carduni  10065  r0weon  10094  dfac8clem  10114  cardinfima  10179  alephfp  10190  iunfictbso  10196  dfac5lem4  10208  dfac2a  10211  dfacacn  10223  dfac12lem2  10226  kmlem2  10233  fin23lem16  10416  fin23lem21  10420  isf32lem5  10438  fin1a2lem11  10491  fin1a2lem13  10493  itunitc  10502  axdc2lem  10529  axdc3lem2  10532  ttukeylem5  10594  ttukeylem6  10595  fpwwe2lem10  10728  fpwwe2lem11  10729  fpwwe2lem12  10730  fpwwe2  10731  wunex2  10826  inatsk  10866  tskuni  10871  suplem1pr  11140  suplem2pr  11141  unirnioo  13583  mrcuni  17800  isacs3lem  18721  mrelatlub  18741  dprd2dlem1  20262  lbsextlem2  21442  eltopss  23230  toponss  23250  isbasis3g  23272  baspartn  23277  bastg  23289  tgcl  23292  fctop  23327  cctop  23329  ppttop  23330  epttop  23332  difopn  23357  ssntr  23381  isopn3  23389  isopn3i  23405  toponmre  23416  neiuni  23445  neiptoptop  23454  resttopon  23484  restopn2  23500  perfopn  23508  pnfnei  23543  mnfnei  23544  ssidcn  23578  lmcnp  23627  pnrmopn  23666  ist1-2  23670  nrmsep  23680  isnrm2  23681  isnrm3  23682  regsep2  23699  cncmp  23715  hauscmplem  23729  hauscmp  23730  conndisj  23739  cnconn  23745  conncompss  23756  islly2  23808  nllyrest  23810  nllyidm  23813  hausllycmp  23818  cldllycmp  23819  lly1stc  23820  comppfsc  23856  kgentopon  23862  kgenss  23867  llycmpkgen2  23874  1stckgen  23878  txuni2  23889  ptpjpre1  23895  ptuni2  23900  ptbasfi  23905  xkouni  23923  txcnpi  23932  ptpjopn  23936  txindis  23958  txnlly  23961  txtube  23964  hausdiag  23969  xkopt  23979  xkococnlem  23983  txconn  24013  qtopuni  24026  qtopkgen  24034  tgqtop  24036  regr1lem  24063  kqreglem1  24065  kqreglem2  24066  kqnrmlem1  24067  kqnrmlem2  24068  hmeoimaf1o  24094  reghmph  24117  nrmhmph  24118  filconn  24207  trfil1  24210  ufildr  24255  flimfil  24293  flimfnfcls  24352  alexsublem  24368  alexsubALTlem3  24373  ustbas2  24549  tgioo  25120  xrtgioo  25131  xrsmopn  25137  opnreen  25156  cnheibor  25281  cnllycmp  25282  lebnumlem1  25287  lebnumlem3  25289  bcthlem5  25654  bcth3  25657  voliunlem1  25876  voliunlem3  25878  volsup  25882  opnmbllem  25927  mbfimaopnlem  25981  lhop  26341  nosupno  28065  noinfno  28080  noetasuplem4  28098  noetainflem4  28102  tglnpt  29017  tglineintmo  29115  ubthlem1  31477  shatomistici  32968  hatomistici  32969  elrspunidl  34024  zarclsiin  34549  tpr2rico  34590  hasheuni  34763  prob01  35091  probdsb  35100  totprobd  35104  probmeasb  35108  cndprobtot  35114  orvcelval  35147  bnj1450  35726  bnj1501  35743  pconnconn  36082  cvmsf1o  36123  cvmscld  36124  cvmsss2  36125  cvmopnlem  36129  cvmfolem  36130  cvmliftmolem1  36132  cvmliftlem6  36141  cvmliftlem8  36143  cvmlift2lem9  36162  cvmlift2lem11  36164  cvmlift2lem12  36165  cvmlift3lem6  36175  cardprcr  36550  dfon2lem3  36639  dfon2lem7  36643  ntruni  37207  clsint2  37209  neibastop1  37239  topmeet  37244  topjoin  37245  fnemeet1  37246  fnejoin1  37248  dfttc2g  37386  opnmbllem0  38667  mbfresfi  38677  heiborlem1  38838  lssats  40162  dicval  42326  mapdunirnN  42800  isnacs3  43814  aomclem4  44152  kelac2  44160  onsupuni  44324  onsupmaxb  44334  mnuunid  45354  mnutrcld  45356  grumnudlem  45362  wfac8prim  46085  ssuniint  46188  stoweidlem28  47131  stoweidlem50  47153  stoweidlem52  47155  stoweidlem53  47156  stoweidlem54  47157  prsal  47421  salincl  47427  saliinclf  47429  saldifcl2  47431  salexct  47437  psmeasurelem  47573  caragenuni  47614  carageniuncl  47626  caratheodorylem1  47629  caratheodorylem2  47630  voncmpl  47724  opncldbid  50109  opndisj  50110  unilbeu  50192