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

Theorem unssd 3988
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 3986 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
43biimpi 207 . 2 ((𝐴𝐶𝐵𝐶) → (𝐴𝐵) ⊆ 𝐶)
51, 2, 4syl2anc 575 1 (𝜑 → (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  cun 3767  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-un 3774  df-in 3776  df-ss 3783
This theorem is referenced by:  uneqdifeq  4253  tpssi  4557  sofld  5792  fr3nr  7205  suceloni  7239  ralxpmap  8140  marypha1lem  8574  wemapso2lem  8692  unwf  8916  rankunb  8956  ackbij1lem6  9328  ackbij1lem16  9338  ssfin4  9413  isfin1-3  9489  ttukeylem7  9618  fpwwe2lem13  9745  wuncval2  9850  inar1  9878  un0addcl  11588  un0mulcl  11589  ssfzunsnext  12605  fzosplit  12721  fzouzsplit  12723  hashf1lem1  13452  ccatrn  13582  trclfvlb3  13971  trclun  13974  relexpfld  14008  saddisj  15402  lcmfunsnlem2lem1  15566  lcmfunsnlem2lem2  15567  lcmfunsnlem2  15568  lcmfun  15573  prmreclem5  15837  4sqlem11  15872  4sqlem19  15880  vdwlem1  15898  vdwlem12  15909  ramub1lem1  15943  ramub1lem2  15944  mrieqvlemd  16490  mreexmrid  16504  mreexexlem2d  16506  mreexexlem3d  16507  mreexexlem4d  16508  acsfiindd  17378  tsrdir  17439  f1omvdco2  18065  symgsssg  18084  symggen  18087  lsmunss  18270  efgsfo  18349  lsptpcl  19182  lspun  19190  lsmsp  19289  lspsolvlem  19346  lspsolv  19347  lsppratlem3  19354  lsppratlem4  19355  islbs3  19360  lbsextlem4  19366  aspval2  19552  evlseu  19720  clslp  21163  neitr  21195  ordtuni  21205  ordtbas2  21206  ordtbas  21207  ordtrest  21217  cmpcld  21416  comppfsc  21546  1stckgenlem  21567  1stckgen  21568  ptbasfi  21595  fbun  21854  trfil2  21901  isufil2  21922  ufileu  21933  filufint  21934  fmfnfm  21972  hausflim  21995  flimclslem  21998  fclsfnflim  22041  flimfnfcls  22042  alexsubALTlem3  22063  alexsubALTlem4  22064  tsmsgsum  22152  tsmsres  22157  tsmsxplem1  22166  ustund  22235  trust  22243  ustuqtop1  22255  prdsdsf  22382  prdsxmetlem  22383  prdsmet  22385  prdsbl  22506  prdsxmslem2  22544  restmetu  22585  icccmplem2  22836  rrxmval  23399  rrxmet  23402  rrxdstprj1  23403  ovolunlem1  23477  ovolunnul  23480  nulmbl2  23516  volun  23525  volcn  23586  itgsplitioo  23817  limcvallem  23848  limcdif  23853  ellimc2  23854  limcres  23863  limccnp  23868  limccnp2  23869  limcco  23870  dvreslem  23886  dvres2lem  23887  dvaddbr  23914  dvmulbr  23915  lhop2  23991  dvcnvrelem2  23994  elply2  24165  plyf  24167  elplyr  24170  elplyd  24171  ply1term  24173  ply0  24177  plyeq0lem  24179  plyeq0  24180  plyaddlem  24184  plymullem  24185  dgrlem  24198  coeidlem  24206  plyco  24210  plycj  24246  aannenlem2  24297  xrlimcnp  24908  perfectlem2  25168  shlej1  28546  shlub  28600  disjiunel  29733  fcoinver  29742  ordtrestNEW  30291  carsggect  30704  eulerpartlemt  30757  hgt750lemb  31058  hgt750leme  31060  bnj1136  31386  bnj1452  31441  erdszelem8  31501  mclsssvlem  31780  mclsax  31787  mclsind  31788  mthmpps  31800  mclsppslem  31801  dftrpred3g  32051  noextend  32138  ssltun1  32234  ssltun2  32235  topjoin  32679  poimirlem32  33752  ftc1anclem7  33801  ftc1anc  33803  prdsbnd  33901  rrnequiv  33943  pclfinN  35678  dochdmj1  37168  djhspss  37184  djhunssN  37187  djhlsmcl  37192  dvh4dimlem  37221  dvhdimlem  37222  lclkrlem2c  37287  lclkrlem2v  37306  mapdh9a  37567  hdmapval0  37611  hdmapval3lemN  37615  hdmap10lem  37617  elrfi  37756  cmpfiiin  37759  istopclsd  37762  mzpcompact2lem  37813  eldioph2lem2  37823  eldioph2  37824  rngunsnply  38241  idomsubgmo  38274  dfrcl2  38463  iunrelexp0  38491  relexp0a  38505  brtrclfv2  38516  frege77d  38535  frege109d  38546  frege131d  38553  clsk3nimkb  38835  isotone1  38843  ntrclskb  38864  ntrclsk3  38865  ntrclsk13  38866  ntrneixb  38890  ntrneix3  38892  ntrneix13  38894  unima  39832  infxrpnf  40150  mccllem  40306  limciccioolb  40330  limcicciooub  40346  limcresiooub  40351  limcresioolb  40352  icccncfext  40577  dvnprodlem2  40639  ovolsplit  40681  fourierdlem20  40820  fourierdlem46  40845  fourierdlem48  40847  fourierdlem49  40848  fourierdlem50  40849  fourierdlem51  40850  fourierdlem54  40853  fourierdlem64  40863  fourierdlem76  40875  fourierdlem101  40900  fourierdlem102  40901  fourierdlem103  40902  fourierdlem104  40903  fourierdlem114  40913  sge0resplit  41099  sge0xaddlem1  41126  ismeannd  41160  caragenuncl  41206  omeunle  41209  isomenndlem  41223  hoidmvlelem2  41289  hoidmvlelem3  41290  hoidmvlelem4  41291  perfectALTVlem2  42203
  Copyright terms: Public domain W3C validator