Theorem unssd 4121

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 4119	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)
4	3	biimpi 217	. 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ∪ 𝐵) ⊆ 𝐶)
5	1, 2, 4	syl2anc 590	1 ⊢ (𝜑 → (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   ∪ cun 3881   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900

This theorem is referenced by:  uneqdifeq  4420  tpssi  4769  sofld  6138  unima  6902  fr3nr  7715  ordsuci  7751  resf1extb  7874  resf1ext2b  7875  xpord2pred  8085  xpord3pred  8092  frrlem13  8238  naddcllem  8602  ralxpmap  8834  marypha1lem  9336  wemapso2lem  9457  unwf  9725  rankunb  9765  ackbij1lem6  10137  ackbij1lem16  10147  ssfin4  10223  isfin1-3  10299  ttukeylem7  10428  fpwwe2lem12  10556  wuncval2  10661  inar1  10689  un0addcl  12461  un0mulcl  12462  ssfzunsnext  13514  fzosplit  13638  fzouzsplit  13640  hashf1lem1  14408  ccatrn  14543  trclfvlb3  14964  trclun  14967  relexpfld  15002  saddisj  16425  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  lcmfunsnlem2  16600  lcmfun  16605  prmreclem5  16882  4sqlem11  16917  4sqlem19  16925  vdwlem1  16943  vdwlem12  16954  ramub1lem1  16988  ramub1lem2  16989  mrieqvlemd  17586  mreexmrid  17600  mreexexlem2d  17602  mreexexlem3d  17603  mreexexlem4d  17604  acsfiindd  18510  tsrdir  18561  f1omvdco2  19414  symgsssg  19433  symggen  19436  lsmunss  19625  efgsfo  19705  lsptpcl  20969  lspun  20977  lsmsp  21076  lspsolvlem  21135  lspsolv  21136  lsppratlem3  21142  lsppratlem4  21143  islbs3  21148  lbsextlem4  21154  aspval2  21873  evlseu  22059  mhpaddcl  22139  clslp  23131  neitr  23163  ordtuni  23173  ordtbas2  23174  ordtbas  23175  ordtrest  23185  cmpcld  23385  comppfsc  23515  1stckgenlem  23536  1stckgen  23537  ptbasfi  23564  fbun  23823  trfil2  23870  isufil2  23891  ufileu  23902  filufint  23903  fmfnfm  23941  hausflim  23964  flimclslem  23967  fclsfnflim  24010  flimfnfcls  24011  alexsubALTlem3  24032  alexsubALTlem4  24033  tsmsgsum  24122  tsmsres  24127  tsmsxplem1  24136  ustund  24205  trust  24212  ustuqtop1  24224  prdsdsf  24350  prdsxmetlem  24351  prdsmet  24353  prdsbl  24474  prdsxmslem2  24512  restmetu  24553  icccmplem2  24807  rrxmval  25390  rrxmet  25393  rrxdstprj1  25394  ovolunlem1  25482  ovolunnul  25485  nulmbl2  25521  volun  25530  volcn  25591  itgsplitioo  25823  limcvallem  25856  limcdif  25861  ellimc2  25862  limcres  25871  limccnp  25876  limccnp2  25877  limcco  25878  dvreslem  25894  dvres2lem  25895  dvaddbr  25923  dvmulbr  25924  lhop2  26000  dvcnvrelem2  26003  elply2  26179  plyf  26181  elplyr  26184  elplyd  26185  ply1term  26187  ply0  26191  plyeq0lem  26193  plyeq0  26194  plyaddlem  26198  plymullem  26199  dgrlem  26212  coeidlem  26220  plyco  26224  plycj  26260  plycjOLD  26262  aannenlem2  26313  xrlimcnp  26950  perfectlem2  27211  noextend  27648  sltsun1  27798  sltsun2  27799  cutlt  27942  lrrecpred  27954  addsproplem2  27980  addsuniflem  28011  addbday  28028  negsid  28051  mulsproplem9  28134  sltmuls1  28157  sltmuls2  28158  precsexlem8  28224  precsexlem11  28227  onaddscl  28287  bdaypw2n0bndlem  28473  shlej1  31449  shlub  31503  disjiunel  32685  fcoinver  32693  gsumzresunsn  33143  gsumwun  33157  elrgspnsubrunlem1  33328  elrgspnsubrunlem2  33329  elrgspnsubrun  33330  lsmidl  33484  elrspunsn  33512  mxidlprm  33553  qsdrngilem  33577  esplyind  33759  lindsun  33809  fldgenfldext  33852  evls1fldgencl  33854  fldextrspunlem1  33859  fldextrspunfld  33860  fldextrspunlem2  33861  fldextrspundgdvdslem  33864  fldextrspundgdvds  33865  algextdeglem1  33901  algextdeglem2  33902  algextdeglem3  33903  algextdeglem4  33904  algextdeglem5  33905  rtelextdg2  33911  constrextdg2lem  33932  constrext2chnlem  33934  constrfiss  33935  constrllcllem  33936  constrlccllem  33937  constrcccllem  33938  ordtrestNEW  34105  carsggect  34502  eulerpartlemt  34555  hgt750lemb  34840  hgt750leme  34842  bnj1136  35179  bnj1452  35234  erdszelem8  35426  mclsssvlem  35790  mclsax  35797  mclsind  35798  mthmpps  35810  mclsppslem  35811  topjoin  36593  weiunse  36696  poimirlem32  38019  ftc1anclem7  38066  ftc1anc  38068  prdsbnd  38160  rrnequiv  38202  pclfinN  40392  dochdmj1  41882  djhspss  41898  djhunssN  41901  djhlsmcl  41906  dvh4dimlem  41935  dvhdimlem  41936  lclkrlem2c  42001  lclkrlem2v  42020  mapdh9a  42281  hdmapval0  42325  hdmapval3lemN  42329  hdmap10lem  42331  deg1gprod  42625  dvun  42836  elrfi  43143  cmpfiiin  43146  istopclsd  43149  mzpcompact2lem  43200  eldioph2lem2  43210  eldioph2  43211  rngunsnply  43614  idomsubgmo  43638  omabs2  43777  dfrcl2  44118  iunrelexp0  44146  relexp0a  44160  brtrclfv2  44171  frege77d  44190  frege109d  44201  frege131d  44208  clsk3nimkb  44484  isotone1  44492  ntrclskb  44513  ntrclsk3  44514  ntrclsk13  44515  ntrneixb  44539  ntrneix3  44541  ntrneix13  44543  infxrpnf  45889  pimxrneun  45931  mccllem  46042  limciccioolb  46066  limcicciooub  46080  limcresiooub  46085  limcresioolb  46086  icccncfext  46330  dvnprodlem2  46390  ovolsplit  46431  fourierdlem20  46570  fourierdlem46  46595  fourierdlem48  46597  fourierdlem49  46598  fourierdlem50  46599  fourierdlem51  46600  fourierdlem54  46603  fourierdlem64  46613  fourierdlem76  46625  fourierdlem101  46650  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem114  46663  sge0resplit  46849  sge0xaddlem1  46876  ismeannd  46910  caragenuncl  46956  omeunle  46959  isomenndlem  46973  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvlelem4  47041  perfectALTVlem2  48213  gpgprismgriedgdmss  48543  pgindlem  50205