Theorem elssuni 4936

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

Syntax hints:   → wi 4   ∈ wcel 2099   ⊆ wss 3945  ∪ cuni 4904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-in 3952  df-ss 3962  df-uni 4905

This theorem is referenced by:  unissel  4937  ssunieq  4942  pwuni  4944  pwel  5376  uniopel  5513  dmrnssfld  5968  unixp0  6282  elfvunirn  6924  fvssunirnOLD  6926  sorpssuni  7732  iunpw  7768  pwuninel2  8274  frrlem8  8293  frrlem10  8295  frrlem14  8299  fprresex  8310  wfrlem12OLD  8335  wfrlem16OLD  8339  wfrlem17OLD  8340  onfununi  8356  tfrlem9  8400  tfrlem9a  8401  tfrlem13  8405  sbthlem1  9102  sbthlem2  9103  2pwuninel  9151  ordunifi  9312  unifpw  9374  fissuni  9376  dffi3  9449  cantnfp1lem3  9698  oemapvali  9702  cantnflem1  9707  cnfcom3lem  9721  rankuni2b  9871  carduni  9999  r0weon  10030  dfac8clem  10050  cardinfima  10115  alephfp  10126  iunfictbso  10132  dfac5lem4  10144  dfac2a  10147  dfacacn  10159  dfac12lem2  10162  kmlem2  10169  fin23lem16  10353  fin23lem21  10357  isf32lem5  10375  fin1a2lem11  10428  fin1a2lem13  10430  itunitc  10439  axdc2lem  10466  axdc3lem2  10469  ttukeylem5  10531  ttukeylem6  10532  fpwwe2lem10  10658  fpwwe2lem11  10659  fpwwe2lem12  10660  fpwwe2  10661  wunex2  10756  inatsk  10796  tskuni  10801  suplem1pr  11070  suplem2pr  11071  unirnioo  13453  mrcuni  17595  isacs3lem  18528  mrelatlub  18548  dprd2dlem1  19992  lbsextlem2  21041  eltopss  22803  toponss  22823  isbasis3g  22846  baspartn  22851  bastg  22863  tgcl  22866  fctop  22901  cctop  22903  ppttop  22904  epttop  22906  difopn  22932  ssntr  22956  isopn3  22964  isopn3i  22980  toponmre  22991  neiuni  23020  neiptoptop  23029  resttopon  23059  restopn2  23075  perfopn  23083  pnfnei  23118  mnfnei  23119  ssidcn  23153  lmcnp  23202  pnrmopn  23241  ist1-2  23245  nrmsep  23255  isnrm2  23256  isnrm3  23257  regsep2  23274  cncmp  23290  hauscmplem  23304  hauscmp  23305  conndisj  23314  cnconn  23320  conncompss  23331  islly2  23382  nllyrest  23384  nllyidm  23387  hausllycmp  23392  cldllycmp  23393  lly1stc  23394  comppfsc  23430  kgentopon  23436  kgenss  23441  llycmpkgen2  23448  1stckgen  23452  txuni2  23463  ptpjpre1  23469  ptuni2  23474  ptbasfi  23479  xkouni  23497  txcnpi  23506  ptpjopn  23510  txindis  23532  txnlly  23535  txtube  23538  hausdiag  23543  xkopt  23553  xkococnlem  23557  txconn  23587  qtopuni  23600  qtopkgen  23608  tgqtop  23610  regr1lem  23637  kqreglem1  23639  kqreglem2  23640  kqnrmlem1  23641  kqnrmlem2  23642  hmeoimaf1o  23668  reghmph  23691  nrmhmph  23692  filconn  23781  trfil1  23784  ufildr  23829  flimfil  23867  flimfnfcls  23926  alexsublem  23942  alexsubALTlem3  23947  ustbas2  24124  tgioo  24706  xrtgioo  24716  xrsmopn  24722  opnreen  24741  cnheibor  24875  cnllycmp  24876  lebnumlem1  24881  lebnumlem3  24883  bcthlem5  25250  bcth3  25253  voliunlem1  25473  voliunlem3  25475  volsup  25479  opnmbllem  25524  mbfimaopnlem  25578  lhop  25943  nosupno  27630  noinfno  27645  noetasuplem4  27663  noetainflem4  27667  tglnpt  28347  tglineintmo  28440  ubthlem1  30674  shatomistici  32165  hatomistici  32166  unifi3  32489  elrspunidl  33139  zarclsiin  33467  tpr2rico  33508  hasheuni  33699  difelsiga  33747  prob01  34028  probdsb  34037  totprobd  34041  probmeasb  34045  cndprobtot  34051  orvcelval  34083  bnj1450  34676  bnj1501  34693  pconnconn  34836  cvmsf1o  34877  cvmscld  34878  cvmsss2  34879  cvmopnlem  34883  cvmfolem  34884  cvmliftmolem1  34886  cvmliftlem6  34895  cvmliftlem8  34897  cvmlift2lem9  34916  cvmlift2lem11  34918  cvmlift2lem12  34919  cvmlift3lem6  34929  dfon2lem3  35376  dfon2lem7  35380  ntruni  35806  clsint2  35808  neibastop1  35838  topmeet  35843  topjoin  35844  fnemeet1  35845  fnejoin1  35847  opnmbllem0  37124  mbfresfi  37134  heiborlem1  37279  lssats  38479  dicval  40644  mapdunirnN  41118  isnacs3  42121  aomclem4  42472  kelac2  42480  onsupuni  42648  onsupmaxb  42658  mnuunid  43705  mnutrcld  43707  grumnudlem  43713  ssuniint  44435  stoweidlem28  45407  stoweidlem50  45429  stoweidlem52  45431  stoweidlem53  45432  stoweidlem54  45433  prsal  45697  salincl  45703  saliinclf  45705  saldifcl2  45707  salexct  45713  psmeasurelem  45849  caragenuni  45890  carageniuncl  45902  caratheodorylem1  45905  caratheodorylem2  45906  voncmpl  46000  opncldeqv  47911  opndisj  47912  unilbeu  47987  setrec1lem2  48110  setrec2fun  48114

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »