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

Theorem unssd 4159
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 4157 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
43biimpi 217 . 2 ((𝐴𝐶𝐵𝐶) → (𝐴𝐵) ⊆ 𝐶)
51, 2, 4syl2anc 584 1 (𝜑 → (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  cun 3931  wss 3933
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 2790
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 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-in 3940  df-ss 3949
This theorem is referenced by:  uneqdifeq  4434  tpssi  4761  sofld  6037  unima  6732  fr3nr  7483  suceloni  7517  ralxpmap  8448  marypha1lem  8885  wemapso2lem  9004  unwf  9227  rankunb  9267  ackbij1lem6  9635  ackbij1lem16  9645  ssfin4  9720  isfin1-3  9796  ttukeylem7  9925  fpwwe2lem13  10052  wuncval2  10157  inar1  10185  un0addcl  11918  un0mulcl  11919  ssfzunsnext  12940  fzosplit  13058  fzouzsplit  13060  hashf1lem1  13801  ccatrn  13931  trclfvlb3  14359  trclun  14362  relexpfld  14396  saddisj  15802  lcmfunsnlem2lem1  15970  lcmfunsnlem2lem2  15971  lcmfunsnlem2  15972  lcmfun  15977  prmreclem5  16244  4sqlem11  16279  4sqlem19  16287  vdwlem1  16305  vdwlem12  16316  ramub1lem1  16350  ramub1lem2  16351  mrieqvlemd  16888  mreexmrid  16902  mreexexlem2d  16904  mreexexlem3d  16905  mreexexlem4d  16906  acsfiindd  17775  tsrdir  17836  f1omvdco2  18505  symgsssg  18524  symggen  18527  lsmunss  18713  efgsfo  18794  lsptpcl  19680  lspun  19688  lsmsp  19787  lspsolvlem  19843  lspsolv  19844  lsppratlem3  19850  lsppratlem4  19851  islbs3  19856  lbsextlem4  19862  aspval2  20055  evlseu  20224  mhpaddcl  20266  clslp  21684  neitr  21716  ordtuni  21726  ordtbas2  21727  ordtbas  21728  ordtrest  21738  cmpcld  21938  comppfsc  22068  1stckgenlem  22089  1stckgen  22090  ptbasfi  22117  fbun  22376  trfil2  22423  isufil2  22444  ufileu  22455  filufint  22456  fmfnfm  22494  hausflim  22517  flimclslem  22520  fclsfnflim  22563  flimfnfcls  22564  alexsubALTlem3  22585  alexsubALTlem4  22586  tsmsgsum  22674  tsmsres  22679  tsmsxplem1  22688  ustund  22757  trust  22765  ustuqtop1  22777  prdsdsf  22904  prdsxmetlem  22905  prdsmet  22907  prdsbl  23028  prdsxmslem2  23066  restmetu  23107  icccmplem2  23358  rrxmval  23935  rrxmet  23938  rrxdstprj1  23939  ovolunlem1  24025  ovolunnul  24028  nulmbl2  24064  volun  24073  volcn  24134  itgsplitioo  24365  limcvallem  24396  limcdif  24401  ellimc2  24402  limcres  24411  limccnp  24416  limccnp2  24417  limcco  24418  dvreslem  24434  dvres2lem  24435  dvaddbr  24462  dvmulbr  24463  lhop2  24539  dvcnvrelem2  24542  elply2  24713  plyf  24715  elplyr  24718  elplyd  24719  ply1term  24721  ply0  24725  plyeq0lem  24727  plyeq0  24728  plyaddlem  24732  plymullem  24733  dgrlem  24746  coeidlem  24754  plyco  24758  plycj  24794  aannenlem2  24845  xrlimcnp  25473  perfectlem2  25733  shlej1  29064  shlub  29118  disjiunel  30274  fcoinver  30285  gsumzresunsn  30618  lindsun  30920  ordtrestNEW  31063  carsggect  31475  eulerpartlemt  31528  hgt750lemb  31826  hgt750leme  31828  bnj1136  32166  bnj1452  32221  erdszelem8  32342  mclsssvlem  32706  mclsax  32713  mclsind  32714  mthmpps  32726  mclsppslem  32727  dftrpred3g  32969  frrlem13  33032  noextend  33070  ssltun1  33166  ssltun2  33167  topjoin  33610  poimirlem32  34805  ftc1anclem7  34854  ftc1anc  34856  prdsbnd  34952  rrnequiv  34994  pclfinN  36916  dochdmj1  38406  djhspss  38422  djhunssN  38425  djhlsmcl  38430  dvh4dimlem  38459  dvhdimlem  38460  lclkrlem2c  38525  lclkrlem2v  38544  mapdh9a  38805  hdmapval0  38849  hdmapval3lemN  38853  hdmap10lem  38855  elrfi  39169  cmpfiiin  39172  istopclsd  39175  mzpcompact2lem  39226  eldioph2lem2  39236  eldioph2  39237  rngunsnply  39651  idomsubgmo  39676  dfrcl2  39897  iunrelexp0  39925  relexp0a  39939  brtrclfv2  39950  frege77d  39969  frege109d  39980  frege131d  39987  clsk3nimkb  40268  isotone1  40276  ntrclskb  40297  ntrclsk3  40298  ntrclsk13  40299  ntrneixb  40323  ntrneix3  40325  ntrneix13  40327  infxrpnf  41597  mccllem  41754  limciccioolb  41778  limcicciooub  41794  limcresiooub  41799  limcresioolb  41800  icccncfext  42046  dvnprodlem2  42108  ovolsplit  42150  fourierdlem20  42289  fourierdlem46  42314  fourierdlem48  42316  fourierdlem49  42317  fourierdlem50  42318  fourierdlem51  42319  fourierdlem54  42322  fourierdlem64  42332  fourierdlem76  42344  fourierdlem101  42369  fourierdlem102  42370  fourierdlem103  42371  fourierdlem104  42372  fourierdlem114  42382  sge0resplit  42565  sge0xaddlem1  42592  ismeannd  42626  caragenuncl  42672  omeunle  42675  isomenndlem  42689  hoidmvlelem2  42755  hoidmvlelem3  42756  hoidmvlelem4  42757  perfectALTVlem2  43764
  Copyright terms: Public domain W3C validator