Theorem elssuni 4901

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3914  ∪ cuni 4871

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-uni 4872

This theorem is referenced by:  unissel  4902  ssunieq  4907  pwuni  4909  pwel  5336  uniopel  5476  dmrnssfld  5937  unixp0  6256  elfvunirn  6890  fvssunirnOLD  6892  sorpssuni  7708  iunpw  7747  pwuninel2  8253  frrlem8  8272  frrlem10  8274  frrlem14  8278  fprresex  8289  onfununi  8310  tfrlem9  8353  tfrlem9a  8354  tfrlem13  8358  sbthlem1  9051  sbthlem2  9052  2pwuninel  9096  ordunifi  9237  unifpw  9306  fissuni  9308  dffi3  9382  cantnfp1lem3  9633  oemapvali  9637  cantnflem1  9642  cnfcom3lem  9656  rankuni2b  9806  carduni  9934  r0weon  9965  dfac8clem  9985  cardinfima  10050  alephfp  10061  iunfictbso  10067  dfac5lem4  10079  dfac5lem4OLD  10081  dfac2a  10083  dfacacn  10095  dfac12lem2  10098  kmlem2  10105  fin23lem16  10288  fin23lem21  10292  isf32lem5  10310  fin1a2lem11  10363  fin1a2lem13  10365  itunitc  10374  axdc2lem  10401  axdc3lem2  10404  ttukeylem5  10466  ttukeylem6  10467  fpwwe2lem10  10593  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  wunex2  10691  inatsk  10731  tskuni  10736  suplem1pr  11005  suplem2pr  11006  unirnioo  13410  mrcuni  17582  isacs3lem  18501  mrelatlub  18521  dprd2dlem1  19973  lbsextlem2  21069  eltopss  22794  toponss  22814  isbasis3g  22836  baspartn  22841  bastg  22853  tgcl  22856  fctop  22891  cctop  22893  ppttop  22894  epttop  22896  difopn  22921  ssntr  22945  isopn3  22953  isopn3i  22969  toponmre  22980  neiuni  23009  neiptoptop  23018  resttopon  23048  restopn2  23064  perfopn  23072  pnfnei  23107  mnfnei  23108  ssidcn  23142  lmcnp  23191  pnrmopn  23230  ist1-2  23234  nrmsep  23244  isnrm2  23245  isnrm3  23246  regsep2  23263  cncmp  23279  hauscmplem  23293  hauscmp  23294  conndisj  23303  cnconn  23309  conncompss  23320  islly2  23371  nllyrest  23373  nllyidm  23376  hausllycmp  23381  cldllycmp  23382  lly1stc  23383  comppfsc  23419  kgentopon  23425  kgenss  23430  llycmpkgen2  23437  1stckgen  23441  txuni2  23452  ptpjpre1  23458  ptuni2  23463  ptbasfi  23468  xkouni  23486  txcnpi  23495  ptpjopn  23499  txindis  23521  txnlly  23524  txtube  23527  hausdiag  23532  xkopt  23542  xkococnlem  23546  txconn  23576  qtopuni  23589  qtopkgen  23597  tgqtop  23599  regr1lem  23626  kqreglem1  23628  kqreglem2  23629  kqnrmlem1  23630  kqnrmlem2  23631  hmeoimaf1o  23657  reghmph  23680  nrmhmph  23681  filconn  23770  trfil1  23773  ufildr  23818  flimfil  23856  flimfnfcls  23915  alexsublem  23931  alexsubALTlem3  23936  ustbas2  24113  tgioo  24684  xrtgioo  24695  xrsmopn  24701  opnreen  24720  cnheibor  24854  cnllycmp  24855  lebnumlem1  24860  lebnumlem3  24862  bcthlem5  25228  bcth3  25231  voliunlem1  25451  voliunlem3  25453  volsup  25457  opnmbllem  25502  mbfimaopnlem  25556  lhop  25921  nosupno  27615  noinfno  27630  noetasuplem4  27648  noetainflem4  27652  tglnpt  28476  tglineintmo  28569  ubthlem1  30799  shatomistici  32290  hatomistici  32291  unifi3  32636  elrspunidl  33399  zarclsiin  33861  tpr2rico  33902  hasheuni  34075  difelsiga  34123  prob01  34404  probdsb  34413  totprobd  34417  probmeasb  34421  cndprobtot  34427  orvcelval  34460  bnj1450  35040  bnj1501  35057  pconnconn  35218  cvmsf1o  35259  cvmscld  35260  cvmsss2  35261  cvmopnlem  35265  cvmfolem  35266  cvmliftmolem1  35268  cvmliftlem6  35277  cvmliftlem8  35279  cvmlift2lem9  35298  cvmlift2lem11  35300  cvmlift2lem12  35301  cvmlift3lem6  35311  dfon2lem3  35773  dfon2lem7  35777  ntruni  36315  clsint2  36317  neibastop1  36347  topmeet  36352  topjoin  36353  fnemeet1  36354  fnejoin1  36356  opnmbllem0  37650  mbfresfi  37660  heiborlem1  37805  lssats  39005  dicval  41170  mapdunirnN  41644  isnacs3  42698  aomclem4  43046  kelac2  43054  onsupuni  43218  onsupmaxb  43228  mnuunid  44266  mnutrcld  44268  grumnudlem  44274  wfac8prim  44992  ssuniint  45072  stoweidlem28  46026  stoweidlem50  46048  stoweidlem52  46050  stoweidlem53  46051  stoweidlem54  46052  prsal  46316  salincl  46322  saliinclf  46324  saldifcl2  46326  salexct  46332  psmeasurelem  46468  caragenuni  46509  carageniuncl  46521  caratheodorylem1  46524  caratheodorylem2  46525  voncmpl  46619  opncldeqv  48890  opndisj  48891  unilbeu  48973  setrec1lem2  49677  setrec2fun  49681