MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssun2 Structured version   Visualization version   GIF version

Theorem ssun2 3810
Description: Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
ssun2 𝐴 ⊆ (𝐵𝐴)

Proof of Theorem ssun2
StepHypRef Expression
1 ssun1 3809 . 2 𝐴 ⊆ (𝐴𝐵)
2 uncom 3790 . 2 (𝐴𝐵) = (𝐵𝐴)
31, 2sseqtri 3670 1 𝐴 ⊆ (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  cun 3605  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-in 3614  df-ss 3621
This theorem is referenced by:  ssun4  3812  elun2  3814  nsspssun  3890  unv  4004  un00  4044  snsspr2  4378  snsstp3  4381  fvrn0  6254  riotassuni  6688  ovima0  6855  unexb  7000  difex2  7011  rnexg  7140  fnsuppres  7367  brtpos0  7404  wfrlem16  7475  oaabs2  7770  domunsncan  8101  mapunen  8170  ac6sfi  8245  unfir  8269  domunfican  8274  iunfi  8295  elfiun  8377  dffi3  8378  hartogslem1  8488  unwdomg  8530  unxpwdom2  8534  unxpwdom  8535  trcl  8642  unwf  8711  rankunb  8751  r0weon  8873  infxpenlem  8874  alephfplem4  8968  cda1dif  9036  cdainflem  9051  infcda  9068  cfsuc  9117  fin1a2lem10  9269  axdc3lem4  9313  ttukeylem7  9375  fpwwe2lem13  9502  canthp1lem2  9513  gchac  9541  wunrn  9589  wunex2  9598  inar1  9635  pnfxr  10130  ltrelxr  10137  un0mulcl  11365  fzdifsuc  12438  hashbclem  13274  hashf1lem1  13277  ccatrn  13407  trclublem  13780  relexprng  13830  fsumsplit  14515  o1fsum  14589  incexclem  14612  fprodsplit  14740  vdwlem5  15736  vdwlem8  15739  ramcl2  15767  srnginvl  16059  lmodvsca  16068  ipssca  16075  ipsvsca  16076  ipsip  16077  phlvsca  16085  phlip  16086  odrngtset  16117  odrngle  16118  odrngds  16119  prdssca  16163  prdsvsca  16167  prdsip  16168  prdsle  16169  prdsds  16171  prdstset  16173  prdshom  16174  prdsco  16175  imasds  16220  imassca  16226  imasvsca  16227  imasip  16228  imastset  16229  imasle  16230  mreexexlemd  16351  mreexexlem2d  16352  mreexexlem3d  16353  drsdirfi  16985  ipolerval  17203  psdmrn  17254  dirge  17284  gsumzsplit  18373  gsumsplit2  18375  gsumzunsnd  18401  gsum2dlem2  18416  dprdfadd  18465  dmdprdsplit2lem  18490  dmdprdsplit2  18491  dmdprdsplit  18492  dprdsplit  18493  ablfac1eulem  18517  pgpfaclem1  18526  lspun  19035  lbsextlem2  19207  lbsextlem3  19208  lbsextlem4  19209  psrbagaddcl  19418  psrsca  19437  psrvscafval  19438  mplsubglem  19482  mplcoe5  19516  opsrtoslem2  19533  cnfldcj  19801  cnfldtset  19802  cnfldle  19803  cnfldds  19804  cnfldunif  19805  ordtbas2  21043  ordtbas  21044  ordtopn1  21046  ordtopn2  21047  leordtval2  21064  icomnfordt  21068  iooordt  21069  perfcls  21217  uncmp  21254  fiuncmp  21255  2ndcdisj2  21308  comppfsc  21383  1stckgenlem  21404  1stckgen  21405  ptbasin  21428  ptbasfi  21432  dfac14lem  21468  dfac14  21469  ptuncnv  21658  ptunhmeo  21659  ptcmpfi  21664  fbun  21691  filconn  21734  isufil2  21759  ufprim  21760  fin1aufil  21783  flimclslem  21835  flimfnfcls  21879  tmdgsum  21946  tsmsgsum  21989  tsmssplit  22002  tsmsxplem1  22003  trust  22080  prdsdsf  22219  prdsmet  22222  prdsbl  22343  cnmpt2pc  22774  rrxmetlem  23236  rrxmet  23237  rrxdstprj1  23238  ovolctb2  23306  ovolfiniun  23315  finiunmbl  23358  volfiniun  23361  uniioombllem3  23399  uniioombllem4  23400  mbfres2  23457  itg2splitlem  23560  itg2split  23561  itgsplit  23647  limcvallem  23680  ellimc2  23686  limccnp  23700  limccnp2  23701  limcco  23702  dvmptfsum  23783  lhop2  23823  lhop  23824  mdegcl  23874  elply2  23997  elplyd  24003  ply1term  24005  ply0  24009  plyaddlem1  24014  plymullem1  24015  plymullem  24017  mtest  24203  xrlimcnp  24740  jensen  24760  fsumharmonic  24783  chtdif  24929  lgsdir2lem3  25097  lgsquadlem2  25151  dchrisumlem2  25224  dchrisum0lem1b  25249  dchrisum0lem1  25250  pntrlog2bndlem6  25317  pntlemf  25339  shsleji  28357  shsval2i  28374  ssjo  28434  sshhococi  28533  gsumle  29907  esumsplit  30243  measun  30402  aean  30435  sxbrsigalem2  30476  bnj970  31143  bnj1137  31189  subfacp1lem2a  31288  subfacp1lem3  31290  subfacp1lem5  31292  erdszelem8  31306  kur14lem7  31320  cvmliftlem10  31402  mrsubvr  31534  noetalem3  31990  refssfne  32478  topjoin  32485  tailf  32495  bj-unrab  33047  bj-2upln1upl  33137  bj-ccinftyssccbar  33235  imadifss  33514  finixpnum  33524  matunitlindflem1  33535  mblfinlem4  33579  prdsbnd  33722  heibor1lem  33738  sspadd2  35420  pclfinN  35504  dochdmj1  36996  mzpcompact2lem  37631  eldioph2  37642  eldioph4b  37692  ttac  37920  pwssplit4  37976  isnumbasgrplem2  37991  isnumbasabl  37993  dfacbasgrp  37995  algsca  38068  algvsca  38069  fiuneneq  38092  rclexi  38239  rtrclex  38241  trclubgNEW  38242  trclexi  38244  rtrclexi  38245  cnvrcl0  38249  cnvtrcl0  38250  dfrtrcl5  38253  trrelsuperrel2dg  38280  dfrcl2  38283  relexp0a  38325  relexpaddss  38327  trclimalb2  38335  frege109d  38366  frege131d  38373  isotone1  38663  iblsplit  40500  fourierdlem46  40687  sge0resplit  40941  sge0split  40944  sge0splitmpt  40946  sge0xaddlem1  40968  sbgoldbo  42000  gsumsplit2f  42468  setrec1  42763  elpglem2  42783
  Copyright terms: Public domain W3C validator