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

Theorem unssd 4161
Description: A deduction showing the union of two subclasses is a subclass. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
unssd.1 (𝜑𝐴𝐶)
unssd.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
unssd (𝜑 → (𝐴𝐵) ⊆ 𝐶)

Proof of Theorem unssd
StepHypRef Expression
1 unssd.1 . 2 (𝜑𝐴𝐶)
2 unssd.2 . 2 (𝜑𝐵𝐶)
3 unss 4159 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
43biimpi 217 . 2 ((𝐴𝐶𝐵𝐶) → (𝐴𝐵) ⊆ 𝐶)
51, 2, 4syl2anc 584 1 (𝜑 → (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  cun 3933  wss 3935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-un 3940  df-in 3942  df-ss 3951
This theorem is referenced by:  uneqdifeq  4436  tpssi  4763  sofld  6038  unima  6733  fr3nr  7482  suceloni  7516  ralxpmap  8449  marypha1lem  8886  wemapso2lem  9005  unwf  9228  rankunb  9268  ackbij1lem6  9636  ackbij1lem16  9646  ssfin4  9721  isfin1-3  9797  ttukeylem7  9926  fpwwe2lem13  10053  wuncval2  10158  inar1  10186  un0addcl  11919  un0mulcl  11920  ssfzunsnext  12942  fzosplit  13060  fzouzsplit  13062  hashf1lem1  13803  ccatrn  13933  trclfvlb3  14361  trclun  14364  relexpfld  14398  saddisj  15804  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  lcmfunsnlem2  15974  lcmfun  15979  prmreclem5  16246  4sqlem11  16281  4sqlem19  16289  vdwlem1  16307  vdwlem12  16318  ramub1lem1  16352  ramub1lem2  16353  mrieqvlemd  16890  mreexmrid  16904  mreexexlem2d  16906  mreexexlem3d  16907  mreexexlem4d  16908  acsfiindd  17777  tsrdir  17838  f1omvdco2  18507  symgsssg  18526  symggen  18529  lsmunss  18715  efgsfo  18796  lsptpcl  19682  lspun  19690  lsmsp  19789  lspsolvlem  19845  lspsolv  19846  lsppratlem3  19852  lsppratlem4  19853  islbs3  19858  lbsextlem4  19864  aspval2  20057  evlseu  20226  mhpaddcl  20268  clslp  21686  neitr  21718  ordtuni  21728  ordtbas2  21729  ordtbas  21730  ordtrest  21740  cmpcld  21940  comppfsc  22070  1stckgenlem  22091  1stckgen  22092  ptbasfi  22119  fbun  22378  trfil2  22425  isufil2  22446  ufileu  22457  filufint  22458  fmfnfm  22496  hausflim  22519  flimclslem  22522  fclsfnflim  22565  flimfnfcls  22566  alexsubALTlem3  22587  alexsubALTlem4  22588  tsmsgsum  22676  tsmsres  22681  tsmsxplem1  22690  ustund  22759  trust  22767  ustuqtop1  22779  prdsdsf  22906  prdsxmetlem  22907  prdsmet  22909  prdsbl  23030  prdsxmslem2  23068  restmetu  23109  icccmplem2  23360  rrxmval  23937  rrxmet  23940  rrxdstprj1  23941  ovolunlem1  24027  ovolunnul  24030  nulmbl2  24066  volun  24075  volcn  24136  itgsplitioo  24367  limcvallem  24398  limcdif  24403  ellimc2  24404  limcres  24413  limccnp  24418  limccnp2  24419  limcco  24420  dvreslem  24436  dvres2lem  24437  dvaddbr  24464  dvmulbr  24465  lhop2  24541  dvcnvrelem2  24544  elply2  24715  plyf  24717  elplyr  24720  elplyd  24721  ply1term  24723  ply0  24727  plyeq0lem  24729  plyeq0  24730  plyaddlem  24734  plymullem  24735  dgrlem  24748  coeidlem  24756  plyco  24760  plycj  24796  aannenlem2  24847  xrlimcnp  25474  perfectlem2  25734  shlej1  29065  shlub  29119  disjiunel  30275  fcoinver  30286  gsumzresunsn  30619  lindsun  30921  ordtrestNEW  31064  carsggect  31476  eulerpartlemt  31529  hgt750lemb  31827  hgt750leme  31829  bnj1136  32167  bnj1452  32222  erdszelem8  32343  mclsssvlem  32707  mclsax  32714  mclsind  32715  mthmpps  32727  mclsppslem  32728  dftrpred3g  32970  frrlem13  33033  noextend  33071  ssltun1  33167  ssltun2  33168  topjoin  33611  poimirlem32  34806  ftc1anclem7  34855  ftc1anc  34857  prdsbnd  34954  rrnequiv  34996  pclfinN  36918  dochdmj1  38408  djhspss  38424  djhunssN  38427  djhlsmcl  38432  dvh4dimlem  38461  dvhdimlem  38462  lclkrlem2c  38527  lclkrlem2v  38546  mapdh9a  38807  hdmapval0  38851  hdmapval3lemN  38855  hdmap10lem  38857  elrfi  39171  cmpfiiin  39174  istopclsd  39177  mzpcompact2lem  39228  eldioph2lem2  39238  eldioph2  39239  rngunsnply  39653  idomsubgmo  39678  dfrcl2  39899  iunrelexp0  39927  relexp0a  39941  brtrclfv2  39952  frege77d  39971  frege109d  39982  frege131d  39989  clsk3nimkb  40270  isotone1  40278  ntrclskb  40299  ntrclsk3  40300  ntrclsk13  40301  ntrneixb  40325  ntrneix3  40327  ntrneix13  40329  infxrpnf  41601  mccllem  41758  limciccioolb  41782  limcicciooub  41798  limcresiooub  41803  limcresioolb  41804  icccncfext  42050  dvnprodlem2  42112  ovolsplit  42154  fourierdlem20  42293  fourierdlem46  42318  fourierdlem48  42320  fourierdlem49  42321  fourierdlem50  42322  fourierdlem51  42323  fourierdlem54  42326  fourierdlem64  42336  fourierdlem76  42348  fourierdlem101  42373  fourierdlem102  42374  fourierdlem103  42375  fourierdlem104  42376  fourierdlem114  42386  sge0resplit  42569  sge0xaddlem1  42596  ismeannd  42630  caragenuncl  42676  omeunle  42679  isomenndlem  42693  hoidmvlelem2  42759  hoidmvlelem3  42760  hoidmvlelem4  42761  perfectALTVlem2  43734
  Copyright terms: Public domain W3C validator