Theorem unssd 4137

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

Step	Hyp	Ref	Expression
1		unssd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)
2		unssd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
3		unss 4135	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)
4	3	biimpi 215	. 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ∪ 𝐵) ⊆ 𝐶)
5	1, 2, 4	syl2anc 585	1 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   ∪ cun 3899   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3444  df-un 3906  df-in 3908  df-ss 3918

This theorem is referenced by:  uneqdifeq  4441  tpssi  4787  sofld  6129  unima  6903  fr3nr  7688  ordsuci  7725  sucexeloniOLD  7727  suceloniOLD  7729  frrlem13  8188  ralxpmap  8759  marypha1lem  9294  wemapso2lem  9413  unwf  9671  rankunb  9711  ackbij1lem6  10086  ackbij1lem16  10096  ssfin4  10171  isfin1-3  10247  ttukeylem7  10376  fpwwe2lem12  10503  wuncval2  10608  inar1  10636  un0addcl  12371  un0mulcl  12372  ssfzunsnext  13406  fzosplit  13525  fzouzsplit  13527  hashf1lem1  14272  hashf1lem1OLD  14273  ccatrn  14396  trclfvlb3  14821  trclun  14824  relexpfld  14859  saddisj  16271  lcmfunsnlem2lem1  16440  lcmfunsnlem2lem2  16441  lcmfunsnlem2  16442  lcmfun  16447  prmreclem5  16718  4sqlem11  16753  4sqlem19  16761  vdwlem1  16779  vdwlem12  16790  ramub1lem1  16824  ramub1lem2  16825  mrieqvlemd  17435  mreexmrid  17449  mreexexlem2d  17451  mreexexlem3d  17452  mreexexlem4d  17453  acsfiindd  18368  tsrdir  18419  f1omvdco2  19152  symgsssg  19171  symggen  19174  lsmunss  19360  efgsfo  19440  lsptpcl  20346  lspun  20354  lsmsp  20453  lspsolvlem  20509  lspsolv  20510  lsppratlem3  20516  lsppratlem4  20517  islbs3  20522  lbsextlem4  20528  aspval2  21207  evlseu  21398  mhpaddcl  21446  clslp  22404  neitr  22436  ordtuni  22446  ordtbas2  22447  ordtbas  22448  ordtrest  22458  cmpcld  22658  comppfsc  22788  1stckgenlem  22809  1stckgen  22810  ptbasfi  22837  fbun  23096  trfil2  23143  isufil2  23164  ufileu  23175  filufint  23176  fmfnfm  23214  hausflim  23237  flimclslem  23240  fclsfnflim  23283  flimfnfcls  23284  alexsubALTlem3  23305  alexsubALTlem4  23306  tsmsgsum  23395  tsmsres  23400  tsmsxplem1  23409  ustund  23478  trust  23486  ustuqtop1  23498  prdsdsf  23625  prdsxmetlem  23626  prdsmet  23628  prdsbl  23752  prdsxmslem2  23790  restmetu  23831  icccmplem2  24091  rrxmval  24674  rrxmet  24677  rrxdstprj1  24678  ovolunlem1  24766  ovolunnul  24769  nulmbl2  24805  volun  24814  volcn  24875  itgsplitioo  25107  limcvallem  25140  limcdif  25145  ellimc2  25146  limcres  25155  limccnp  25160  limccnp2  25161  limcco  25162  dvreslem  25178  dvres2lem  25179  dvaddbr  25207  dvmulbr  25208  lhop2  25284  dvcnvrelem2  25287  elply2  25462  plyf  25464  elplyr  25467  elplyd  25468  ply1term  25470  ply0  25474  plyeq0lem  25476  plyeq0  25477  plyaddlem  25481  plymullem  25482  dgrlem  25495  coeidlem  25503  plyco  25507  plycj  25543  aannenlem2  25594  xrlimcnp  26223  perfectlem2  26483  noextend  26919  ssltun1  27052  ssltun2  27053  shlej1  30009  shlub  30063  disjiunel  31220  fcoinver  31231  gsumzresunsn  31599  lsmidl  31884  mxidlprm  31935  lindsun  32002  ordtrestNEW  32167  carsggect  32583  eulerpartlemt  32636  hgt750lemb  32934  hgt750leme  32936  bnj1136  33274  bnj1452  33329  erdszelem8  33457  mclsssvlem  33821  mclsax  33828  mclsind  33829  mthmpps  33841  mclsppslem  33842  xpord2pred  34074  xpord3pred  34080  naddcllem  34114  lrrecpred  34209  addsproplem2  34234  addsunif  34256  topjoin  34691  poimirlem32  35965  ftc1anclem7  36012  ftc1anc  36014  prdsbnd  36107  rrnequiv  36149  pclfinN  38219  dochdmj1  39709  djhspss  39725  djhunssN  39728  djhlsmcl  39733  dvh4dimlem  39762  dvhdimlem  39763  lclkrlem2c  39828  lclkrlem2v  39847  mapdh9a  40108  hdmapval0  40152  hdmapval3lemN  40156  hdmap10lem  40158  elrfi  40829  cmpfiiin  40832  istopclsd  40835  mzpcompact2lem  40886  eldioph2lem2  40896  eldioph2  40897  rngunsnply  41312  idomsubgmo  41337  omabs2  41369  dfrcl2  41655  iunrelexp0  41683  relexp0a  41697  brtrclfv2  41708  frege77d  41727  frege109d  41738  frege131d  41745  clsk3nimkb  42023  isotone1  42031  ntrclskb  42052  ntrclsk3  42053  ntrclsk13  42054  ntrneixb  42078  ntrneix3  42080  ntrneix13  42082  infxrpnf  43373  pimxrneun  43416  mccllem  43526  limciccioolb  43550  limcicciooub  43566  limcresiooub  43571  limcresioolb  43572  icccncfext  43816  dvnprodlem2  43876  ovolsplit  43917  fourierdlem20  44056  fourierdlem46  44081  fourierdlem48  44083  fourierdlem49  44084  fourierdlem50  44085  fourierdlem51  44086  fourierdlem54  44089  fourierdlem64  44099  fourierdlem76  44111  fourierdlem101  44136  fourierdlem102  44137  fourierdlem103  44138  fourierdlem104  44139  fourierdlem114  44149  sge0resplit  44333  sge0xaddlem1  44360  ismeannd  44394  caragenuncl  44440  omeunle  44443  isomenndlem  44457  hoidmvlelem2  44523  hoidmvlelem3  44524  hoidmvlelem4  44525  perfectALTVlem2  45592