Theorem elssuni 4913

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3926  ∪ cuni 4883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-uni 4884

This theorem is referenced by:  unissel  4914  ssunieq  4919  pwuni  4921  pwel  5351  uniopel  5491  dmrnssfld  5953  unixp0  6272  elfvunirn  6908  fvssunirnOLD  6910  sorpssuni  7726  iunpw  7765  pwuninel2  8273  frrlem8  8292  frrlem10  8294  frrlem14  8298  fprresex  8309  wfrlem12OLD  8334  wfrlem16OLD  8338  wfrlem17OLD  8339  onfununi  8355  tfrlem9  8399  tfrlem9a  8400  tfrlem13  8404  sbthlem1  9097  sbthlem2  9098  2pwuninel  9146  ordunifi  9298  unifpw  9367  fissuni  9369  dffi3  9443  cantnfp1lem3  9694  oemapvali  9698  cantnflem1  9703  cnfcom3lem  9717  rankuni2b  9867  carduni  9995  r0weon  10026  dfac8clem  10046  cardinfima  10111  alephfp  10122  iunfictbso  10128  dfac5lem4  10140  dfac5lem4OLD  10142  dfac2a  10144  dfacacn  10156  dfac12lem2  10159  kmlem2  10166  fin23lem16  10349  fin23lem21  10353  isf32lem5  10371  fin1a2lem11  10424  fin1a2lem13  10426  itunitc  10435  axdc2lem  10462  axdc3lem2  10465  ttukeylem5  10527  ttukeylem6  10528  fpwwe2lem10  10654  fpwwe2lem11  10655  fpwwe2lem12  10656  fpwwe2  10657  wunex2  10752  inatsk  10792  tskuni  10797  suplem1pr  11066  suplem2pr  11067  unirnioo  13466  mrcuni  17633  isacs3lem  18552  mrelatlub  18572  dprd2dlem1  20024  lbsextlem2  21120  eltopss  22845  toponss  22865  isbasis3g  22887  baspartn  22892  bastg  22904  tgcl  22907  fctop  22942  cctop  22944  ppttop  22945  epttop  22947  difopn  22972  ssntr  22996  isopn3  23004  isopn3i  23020  toponmre  23031  neiuni  23060  neiptoptop  23069  resttopon  23099  restopn2  23115  perfopn  23123  pnfnei  23158  mnfnei  23159  ssidcn  23193  lmcnp  23242  pnrmopn  23281  ist1-2  23285  nrmsep  23295  isnrm2  23296  isnrm3  23297  regsep2  23314  cncmp  23330  hauscmplem  23344  hauscmp  23345  conndisj  23354  cnconn  23360  conncompss  23371  islly2  23422  nllyrest  23424  nllyidm  23427  hausllycmp  23432  cldllycmp  23433  lly1stc  23434  comppfsc  23470  kgentopon  23476  kgenss  23481  llycmpkgen2  23488  1stckgen  23492  txuni2  23503  ptpjpre1  23509  ptuni2  23514  ptbasfi  23519  xkouni  23537  txcnpi  23546  ptpjopn  23550  txindis  23572  txnlly  23575  txtube  23578  hausdiag  23583  xkopt  23593  xkococnlem  23597  txconn  23627  qtopuni  23640  qtopkgen  23648  tgqtop  23650  regr1lem  23677  kqreglem1  23679  kqreglem2  23680  kqnrmlem1  23681  kqnrmlem2  23682  hmeoimaf1o  23708  reghmph  23731  nrmhmph  23732  filconn  23821  trfil1  23824  ufildr  23869  flimfil  23907  flimfnfcls  23966  alexsublem  23982  alexsubALTlem3  23987  ustbas2  24164  tgioo  24735  xrtgioo  24746  xrsmopn  24752  opnreen  24771  cnheibor  24905  cnllycmp  24906  lebnumlem1  24911  lebnumlem3  24913  bcthlem5  25280  bcth3  25283  voliunlem1  25503  voliunlem3  25505  volsup  25509  opnmbllem  25554  mbfimaopnlem  25608  lhop  25973  nosupno  27667  noinfno  27682  noetasuplem4  27700  noetainflem4  27704  tglnpt  28528  tglineintmo  28621  ubthlem1  30851  shatomistici  32342  hatomistici  32343  unifi3  32690  elrspunidl  33443  zarclsiin  33902  tpr2rico  33943  hasheuni  34116  difelsiga  34164  prob01  34445  probdsb  34454  totprobd  34458  probmeasb  34462  cndprobtot  34468  orvcelval  34501  bnj1450  35081  bnj1501  35098  pconnconn  35253  cvmsf1o  35294  cvmscld  35295  cvmsss2  35296  cvmopnlem  35300  cvmfolem  35301  cvmliftmolem1  35303  cvmliftlem6  35312  cvmliftlem8  35314  cvmlift2lem9  35333  cvmlift2lem11  35335  cvmlift2lem12  35336  cvmlift3lem6  35346  dfon2lem3  35803  dfon2lem7  35807  ntruni  36345  clsint2  36347  neibastop1  36377  topmeet  36382  topjoin  36383  fnemeet1  36384  fnejoin1  36386  opnmbllem0  37680  mbfresfi  37690  heiborlem1  37835  lssats  39030  dicval  41195  mapdunirnN  41669  isnacs3  42733  aomclem4  43081  kelac2  43089  onsupuni  43253  onsupmaxb  43263  mnuunid  44301  mnutrcld  44303  grumnudlem  44309  wfac8prim  45027  ssuniint  45102  stoweidlem28  46057  stoweidlem50  46079  stoweidlem52  46081  stoweidlem53  46082  stoweidlem54  46083  prsal  46347  salincl  46353  saliinclf  46355  saldifcl2  46357  salexct  46363  psmeasurelem  46499  caragenuni  46540  carageniuncl  46552  caratheodorylem1  46555  caratheodorylem2  46556  voncmpl  46650  opncldeqv  48876  opndisj  48877  unilbeu  48959  setrec1lem2  49552  setrec2fun  49556