Theorem elssuni 4905

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3906  ∪ cuni 4873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-uni 4874

This theorem is referenced by:  unissel  4906  ssunieq  4910  pwuni  4912  pwel  5354  uniopel  5501  dmrnssfld  5966  unixp0  6286  elfvunirn  6913  sorpssuni  7731  iunpw  7771  pwuninel2  8271  pwuninel  8272  frrlem8  8291  frrlem10  8293  frrlem14  8297  fprresex  8308  onfununi  8329  tfrlem9  8373  tfrlem9a  8374  tfrlem13  8378  sbthlem1  9076  sbthlem2  9077  2pwuninel  9121  ordunifi  9251  unifpw  9313  fissuni  9315  unifi3  9320  dffi3  9392  cantnfp1lem3  9650  oemapvali  9654  cantnflem1  9659  cnfcom3lem  9673  rankuni2b  9826  carduni  9968  r0weon  9997  dfac8clem  10017  cardinfima  10082  alephfp  10093  iunfictbso  10099  dfac5lem4  10111  dfac2a  10114  dfacacn  10126  dfac12lem2  10129  kmlem2  10136  fin23lem16  10320  fin23lem21  10324  isf32lem5  10342  fin1a2lem11  10395  fin1a2lem13  10397  itunitc  10406  axdc2lem  10433  axdc3lem2  10436  ttukeylem5  10498  ttukeylem6  10499  fpwwe2lem10  10626  fpwwe2lem11  10627  fpwwe2lem12  10628  fpwwe2  10629  wunex2  10724  inatsk  10764  tskuni  10769  suplem1pr  11038  suplem2pr  11039  unirnioo  13477  mrcuni  17678  isacs3lem  18599  mrelatlub  18619  dprd2dlem1  20114  lbsextlem2  21264  eltopss  23045  toponss  23065  isbasis3g  23087  baspartn  23092  bastg  23104  tgcl  23107  fctop  23142  cctop  23144  ppttop  23145  epttop  23147  difopn  23172  ssntr  23196  isopn3  23204  isopn3i  23220  toponmre  23231  neiuni  23260  neiptoptop  23269  resttopon  23299  restopn2  23315  perfopn  23323  pnfnei  23358  mnfnei  23359  ssidcn  23393  lmcnp  23442  pnrmopn  23481  ist1-2  23485  nrmsep  23495  isnrm2  23496  isnrm3  23497  regsep2  23514  cncmp  23530  hauscmplem  23544  hauscmp  23545  conndisj  23554  cnconn  23560  conncompss  23571  islly2  23622  nllyrest  23624  nllyidm  23627  hausllycmp  23632  cldllycmp  23633  lly1stc  23634  comppfsc  23670  kgentopon  23676  kgenss  23681  llycmpkgen2  23688  1stckgen  23692  txuni2  23703  ptpjpre1  23709  ptuni2  23714  ptbasfi  23719  xkouni  23737  txcnpi  23746  ptpjopn  23750  txindis  23772  txnlly  23775  txtube  23778  hausdiag  23783  xkopt  23793  xkococnlem  23797  txconn  23827  qtopuni  23840  qtopkgen  23848  tgqtop  23850  regr1lem  23877  kqreglem1  23879  kqreglem2  23880  kqnrmlem1  23881  kqnrmlem2  23882  hmeoimaf1o  23908  reghmph  23931  nrmhmph  23932  filconn  24021  trfil1  24024  ufildr  24069  flimfil  24107  flimfnfcls  24166  alexsublem  24182  alexsubALTlem3  24187  ustbas2  24363  tgioo  24934  xrtgioo  24945  xrsmopn  24951  opnreen  24970  cnheibor  25095  cnllycmp  25096  lebnumlem1  25101  lebnumlem3  25103  bcthlem5  25468  bcth3  25471  voliunlem1  25690  voliunlem3  25692  volsup  25696  opnmbllem  25741  mbfimaopnlem  25795  lhop  26156  nosupno  27845  noinfno  27860  noetasuplem4  27878  noetainflem4  27882  tglnpt  28796  tglineintmo  28893  ubthlem1  31200  shatomistici  32691  hatomistici  32692  elrspunidl  33714  zarclsiin  34239  tpr2rico  34280  hasheuni  34453  difelsiga  34501  prob01  34781  probdsb  34790  totprobd  34794  probmeasb  34798  cndprobtot  34804  orvcelval  34837  bnj1450  35416  bnj1501  35433  elwf  35468  pconnconn  35701  cvmsf1o  35742  cvmscld  35743  cvmsss2  35744  cvmopnlem  35748  cvmfolem  35749  cvmliftmolem1  35751  cvmliftlem6  35760  cvmliftlem8  35762  cvmlift2lem9  35781  cvmlift2lem11  35783  cvmlift2lem12  35784  cvmlift3lem6  35794  dfon2lem3  36253  dfon2lem7  36257  ntruni  36816  clsint2  36818  neibastop1  36848  topmeet  36853  topjoin  36854  fnemeet1  36855  fnejoin1  36857  dfttc2g  36995  opnmbllem0  38285  mbfresfi  38295  heiborlem1  38440  lssats  39764  dicval  41928  mapdunirnN  42402  isnacs3  43421  aomclem4  43764  kelac2  43772  onsupuni  43936  onsupmaxb  43946  mnuunid  44967  mnutrcld  44969  grumnudlem  44975  wfac8prim  45691  ssuniint  45778  stoweidlem28  46722  stoweidlem50  46744  stoweidlem52  46746  stoweidlem53  46747  stoweidlem54  46748  prsal  47012  salincl  47018  saliinclf  47020  saldifcl2  47022  salexct  47028  psmeasurelem  47164  caragenuni  47205  carageniuncl  47217  caratheodorylem1  47220  caratheodorylem2  47221  voncmpl  47315  opncldeqv  49657  opndisj  49658  unilbeu  49740  setrec1lem2  50443  setrec2fun  50447