MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssun1 Unicode version

Theorem ssun1 3351
Description: Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ssun1  |-  A  C_  ( A  u.  B
)

Proof of Theorem ssun1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 orc 374 . . 3  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
2 elun 3329 . . 3  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
31, 2sylibr 203 . 2  |-  ( x  e.  A  ->  x  e.  ( A  u.  B
) )
43ssriv 3197 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    \/ wo 357    e. wcel 1696    u. cun 3163    C_ wss 3165
This theorem is referenced by:  ssun2  3352  ssun3  3353  elun1  3355  inabs  3413  reuun1  3463  un00  3503  snsspr1  3780  snsstp1  3782  snsstp2  3783  uniintsn  3915  sssucid  4485  unexb  4536  dmexg  4955  sofld  5137  fvrn0  5566  dftpos2  6267  tpostpos2  6271  riotassuni  6359  tfrlem11  6420  oaabs2  6659  ersym  6688  domss2  7036  mapunen  7046  ac6sfi  7117  frfi  7118  unfir  7141  domunfican  7145  iunfi  7160  finsschain  7178  elfiun  7199  dffi3  7200  unwdomg  7314  unxpwdom2  7318  unxpwdom  7319  cantnfp1lem1  7396  cantnfp1lem3  7398  tc2  7443  unwf  7498  rankunb  7538  r0weon  7656  infxpenlem  7657  dfac2  7773  cdadom3  7830  cdainflem  7833  infunabs  7849  infcda  7850  infdif  7851  ackbij1lem15  7876  ackbij1lem16  7877  cfsmolem  7912  isfin4-3  7957  fin23lem11  7959  fin1a2lem10  8051  fin1a2lem13  8054  axdc3lem4  8095  axcclem  8099  zornn0g  8148  ttukeylem1  8152  ttukeylem5  8156  ttukeylem7  8158  fingch  8261  fpwwe2lem13  8280  gchac  8311  wunfi  8359  wundm  8366  wunex2  8376  inar1  8413  ressxr  8892  nnssnn0  9984  un0addcl  10013  un0mulcl  10014  hashbclem  11406  hashf1lem1  11409  hashf1lem2  11410  ccatfn  11443  fsumsplit  12228  sumsplit  12247  fsum2d  12250  fsumabs  12275  fsumrlim  12285  fsumo1  12286  fsumiun  12295  incexclem  12311  vdwapid1  13038  vdwlem6  13049  ramcl2  13079  isstruct2  13173  srngbase  13280  srngplusg  13281  srngmulr  13282  lmodbase  13289  lmodplusg  13290  lmodsca  13291  algbase  13294  algaddg  13295  algmulr  13296  phlbase  13304  phlplusg  13305  phlsca  13306  odrngbas  13328  odrngplusg  13329  odrngmulr  13330  prdssca  13372  prdsbas  13373  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  prdsle  13377  prdsds  13379  prdstset  13381  imasbas  13431  imasplusg  13436  imasmulr  13437  imassca  13438  imasvsca  13439  mreexexlem2d  13563  yonedalem1  14062  yonedalem21  14063  yonedalem22  14068  yonffthlem  14072  drsdirfi  14088  ipobas  14274  ipotset  14276  acsfiindd  14296  psdmrn  14332  dirdm  14372  gsumzaddlem  15219  gsumzsplit  15222  gsumsplit2  15224  gsum2d  15239  dprdfadd  15271  dmdprdsplit2lem  15296  dmdprdsplit2  15297  dmdprdsplit  15298  dprdsplit  15299  ablfac1eulem  15323  lspun  15760  lsmsp  15855  lspsolv  15912  lsppratlem3  15918  islbs3  15924  lbsextlem2  15928  lbsextlem4  15930  psrbagaddcl  16132  psrbas  16140  psrplusg  16142  psrmulr  16145  mplsubglem  16195  mplcoe1  16225  mplcoe2  16227  cnfldbas  16399  cnfldadd  16400  cnfldmul  16401  cnfldcj  16402  basdif0  16707  tgdif0  16746  ordtbas2  16937  ordtbas  16938  ordtopn1  16940  leordtval2  16958  iocpnfordt  16961  icomnfordt  16962  uncmp  17146  fiuncmp  17147  1stckgenlem  17264  1stckgen  17265  ptbasin  17288  ptbasfi  17292  dfac14lem  17327  dfac14  17328  ptuncnv  17514  ptunhmeo  17515  ptcmpfi  17520  fbun  17551  trfil2  17598  isufil2  17619  ufprim  17620  ufileu  17630  filufint  17631  ufildr  17642  fmfnfm  17669  hausflim  17692  flimclslem  17695  fclsfnflim  17738  flimfnfcls  17739  alexsubALTlem4  17760  tmdgsum  17794  tsmsgsum  17837  tsmsres  17842  tsmssplit  17850  tsmsxplem1  17851  prdsxmetlem  17948  imasdsf1olem  17953  prdsbl  18053  icccmplem2  18344  fsumcn  18390  cnmpt2pc  18442  iccpnfcnv  18458  ovolctb2  18867  ovolunnul  18875  ovolfiniun  18876  nulmbl2  18910  finiunmbl  18917  volfiniun  18920  icombl  18937  ioombl  18938  uniiccdif  18949  mbfres2  19016  itg2splitlem  19119  itg2split  19120  itgfsum  19197  itgsplit  19206  itgsplitioo  19208  limcdif  19242  dvreslem  19275  dvaddbr  19303  dvmulbr  19304  dvmptfsum  19338  lhop  19379  dvcnvrelem2  19381  mdegcl  19471  elplyr  19599  plyrem  19701  xrlimcnp  20279  jensenlem1  20297  jensenlem2  20298  jensen  20299  fsumharmonic  20321  chtdif  20412  lgsdir2lem3  20580  lgsquadlem2  20610  dchrisum0lem1b  20680  pntrlog2bndlem6  20748  pntlemf  20770  ex-ss  20830  shsleji  21965  shsval2i  21982  ssjo  22042  sshhococi  22141  esumsplit  23446  subfacp1lem2b  23727  subfacp1lem3  23728  subfacp1lem5  23730  kur14lem7  23758  kur14lem9  23760  cvmliftlem10  23840  dftrpred3g  24307  wfrlem14  24340  wfrlem15  24341  nofulllem4  24430  domfldrefc  25160  prl  25270  basexre  25625  islimrs4  25685  segray  26258  refssfne  26397  locfincmp  26407  comppfsc  26410  filnetlem3  26432  prdsbnd  26620  heibor1lem  26636  rrnequiv  26662  ralxpmap  26864  elrfi  26872  mzpcompact2lem  26932  eldioph2  26944  eldioph4b  26997  ttac  27232  pwssplit4  27294  pwslnmlem2  27298  isnumbasgrplem2  27372  rngunsnply  27481  fiuneneq  27616  idomsubgmo  27617  compne  27745  bnj931  29118  paddunssN  30619  sspadd1  30626  sspadd2  30627  pclfinN  30711  dochdmj1  32202  dvhdimlem  32256
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator