Theorem elssuni 4896

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3903  ∪ cuni 4865

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-uni 4866

This theorem is referenced by:  unissel  4897  ssunieq  4901  pwuni  4903  pwel  5328  uniopel  5472  dmrnssfld  5931  unixp0  6249  elfvunirn  6872  sorpssuni  7687  iunpw  7726  pwuninel2  8226  frrlem8  8245  frrlem10  8247  frrlem14  8251  fprresex  8262  onfununi  8283  tfrlem9  8326  tfrlem9a  8327  tfrlem13  8331  sbthlem1  9027  sbthlem2  9028  2pwuninel  9072  ordunifi  9202  unifpw  9267  fissuni  9269  unifi3  9274  dffi3  9346  cantnfp1lem3  9601  oemapvali  9605  cantnflem1  9610  cnfcom3lem  9624  rankuni2b  9777  carduni  9905  r0weon  9934  dfac8clem  9954  cardinfima  10019  alephfp  10030  iunfictbso  10036  dfac5lem4  10048  dfac5lem4OLD  10050  dfac2a  10052  dfacacn  10064  dfac12lem2  10067  kmlem2  10074  fin23lem16  10257  fin23lem21  10261  isf32lem5  10279  fin1a2lem11  10332  fin1a2lem13  10334  itunitc  10343  axdc2lem  10370  axdc3lem2  10373  ttukeylem5  10435  ttukeylem6  10436  fpwwe2lem10  10563  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  wunex2  10661  inatsk  10701  tskuni  10706  suplem1pr  10975  suplem2pr  10976  unirnioo  13377  mrcuni  17556  isacs3lem  18477  mrelatlub  18497  dprd2dlem1  19984  lbsextlem2  21126  eltopss  22863  toponss  22883  isbasis3g  22905  baspartn  22910  bastg  22922  tgcl  22925  fctop  22960  cctop  22962  ppttop  22963  epttop  22965  difopn  22990  ssntr  23014  isopn3  23022  isopn3i  23038  toponmre  23049  neiuni  23078  neiptoptop  23087  resttopon  23117  restopn2  23133  perfopn  23141  pnfnei  23176  mnfnei  23177  ssidcn  23211  lmcnp  23260  pnrmopn  23299  ist1-2  23303  nrmsep  23313  isnrm2  23314  isnrm3  23315  regsep2  23332  cncmp  23348  hauscmplem  23362  hauscmp  23363  conndisj  23372  cnconn  23378  conncompss  23389  islly2  23440  nllyrest  23442  nllyidm  23445  hausllycmp  23450  cldllycmp  23451  lly1stc  23452  comppfsc  23488  kgentopon  23494  kgenss  23499  llycmpkgen2  23506  1stckgen  23510  txuni2  23521  ptpjpre1  23527  ptuni2  23532  ptbasfi  23537  xkouni  23555  txcnpi  23564  ptpjopn  23568  txindis  23590  txnlly  23593  txtube  23596  hausdiag  23601  xkopt  23611  xkococnlem  23615  txconn  23645  qtopuni  23658  qtopkgen  23666  tgqtop  23668  regr1lem  23695  kqreglem1  23697  kqreglem2  23698  kqnrmlem1  23699  kqnrmlem2  23700  hmeoimaf1o  23726  reghmph  23749  nrmhmph  23750  filconn  23839  trfil1  23842  ufildr  23887  flimfil  23925  flimfnfcls  23984  alexsublem  24000  alexsubALTlem3  24005  ustbas2  24181  tgioo  24752  xrtgioo  24763  xrsmopn  24769  opnreen  24788  cnheibor  24922  cnllycmp  24923  lebnumlem1  24928  lebnumlem3  24930  bcthlem5  25296  bcth3  25299  voliunlem1  25519  voliunlem3  25521  volsup  25525  opnmbllem  25570  mbfimaopnlem  25624  lhop  25989  nosupno  27683  noinfno  27698  noetasuplem4  27716  noetainflem4  27720  tglnpt  28633  tglineintmo  28726  ubthlem1  30957  shatomistici  32448  hatomistici  32449  elrspunidl  33520  zarclsiin  34048  tpr2rico  34089  hasheuni  34262  difelsiga  34310  prob01  34590  probdsb  34599  totprobd  34603  probmeasb  34607  cndprobtot  34613  orvcelval  34646  bnj1450  35225  bnj1501  35242  elwf  35272  pconnconn  35444  cvmsf1o  35485  cvmscld  35486  cvmsss2  35487  cvmopnlem  35491  cvmfolem  35492  cvmliftmolem1  35494  cvmliftlem6  35503  cvmliftlem8  35505  cvmlift2lem9  35524  cvmlift2lem11  35526  cvmlift2lem12  35527  cvmlift3lem6  35537  dfon2lem3  35996  dfon2lem7  36000  ntruni  36540  clsint2  36542  neibastop1  36572  topmeet  36577  topjoin  36578  fnemeet1  36579  fnejoin1  36581  opnmbllem0  37901  mbfresfi  37911  heiborlem1  38056  lssats  39382  dicval  41546  mapdunirnN  42020  isnacs3  43061  aomclem4  43408  kelac2  43416  onsupuni  43580  onsupmaxb  43590  mnuunid  44627  mnutrcld  44629  grumnudlem  44635  wfac8prim  45352  ssuniint  45432  stoweidlem28  46380  stoweidlem50  46402  stoweidlem52  46404  stoweidlem53  46405  stoweidlem54  46406  prsal  46670  salincl  46676  saliinclf  46678  saldifcl2  46680  salexct  46686  psmeasurelem  46822  caragenuni  46863  carageniuncl  46875  caratheodorylem1  46878  caratheodorylem2  46879  voncmpl  46973  opncldeqv  49255  opndisj  49256  unilbeu  49338  setrec1lem2  50041  setrec2fun  50045