Theorem unssd 4151

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3909   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-ss 3928

This theorem is referenced by:  uneqdifeq  4452  tpssi  4798  sofld  6148  unima  6918  fr3nr  7728  ordsuci  7764  sucexeloniOLD  7766  resf1extb  7890  resf1ext2b  7891  xpord2pred  8101  xpord3pred  8108  frrlem13  8254  naddcllem  8617  ralxpmap  8846  marypha1lem  9360  wemapso2lem  9481  unwf  9739  rankunb  9779  ackbij1lem6  10153  ackbij1lem16  10163  ssfin4  10239  isfin1-3  10315  ttukeylem7  10444  fpwwe2lem12  10571  wuncval2  10676  inar1  10704  un0addcl  12451  un0mulcl  12452  ssfzunsnext  13506  fzosplit  13629  fzouzsplit  13631  hashf1lem1  14396  ccatrn  14530  trclfvlb3  14953  trclun  14956  relexpfld  14991  saddisj  16411  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  lcmfunsnlem2  16586  lcmfun  16591  prmreclem5  16867  4sqlem11  16902  4sqlem19  16910  vdwlem1  16928  vdwlem12  16939  ramub1lem1  16973  ramub1lem2  16974  mrieqvlemd  17570  mreexmrid  17584  mreexexlem2d  17586  mreexexlem3d  17587  mreexexlem4d  17588  acsfiindd  18494  tsrdir  18545  f1omvdco2  19362  symgsssg  19381  symggen  19384  lsmunss  19573  efgsfo  19653  lsptpcl  20917  lspun  20925  lsmsp  21025  lspsolvlem  21084  lspsolv  21085  lsppratlem3  21091  lsppratlem4  21092  islbs3  21097  lbsextlem4  21103  aspval2  21840  evlseu  22023  mhpaddcl  22071  clslp  23068  neitr  23100  ordtuni  23110  ordtbas2  23111  ordtbas  23112  ordtrest  23122  cmpcld  23322  comppfsc  23452  1stckgenlem  23473  1stckgen  23474  ptbasfi  23501  fbun  23760  trfil2  23807  isufil2  23828  ufileu  23839  filufint  23840  fmfnfm  23878  hausflim  23901  flimclslem  23904  fclsfnflim  23947  flimfnfcls  23948  alexsubALTlem3  23969  alexsubALTlem4  23970  tsmsgsum  24059  tsmsres  24064  tsmsxplem1  24073  ustund  24142  trust  24150  ustuqtop1  24162  prdsdsf  24288  prdsxmetlem  24289  prdsmet  24291  prdsbl  24412  prdsxmslem2  24450  restmetu  24491  icccmplem2  24745  rrxmval  25338  rrxmet  25341  rrxdstprj1  25342  ovolunlem1  25431  ovolunnul  25434  nulmbl2  25470  volun  25479  volcn  25540  itgsplitioo  25772  limcvallem  25805  limcdif  25810  ellimc2  25811  limcres  25820  limccnp  25825  limccnp2  25826  limcco  25827  dvreslem  25843  dvres2lem  25844  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  lhop2  25953  dvcnvrelem2  25956  elply2  26134  plyf  26136  elplyr  26139  elplyd  26140  ply1term  26142  ply0  26146  plyeq0lem  26148  plyeq0  26149  plyaddlem  26153  plymullem  26154  dgrlem  26167  coeidlem  26175  plyco  26179  plycj  26216  plycjOLD  26218  aannenlem2  26270  xrlimcnp  26911  perfectlem2  27174  noextend  27611  ssltun1  27754  ssltun2  27755  cutlt  27880  lrrecpred  27891  addsproplem2  27917  addsuniflem  27948  addsbday  27964  negsid  27987  mulsproplem9  28067  ssltmul1  28090  ssltmul2  28091  precsexlem8  28156  precsexlem11  28159  onaddscl  28214  shlej1  31339  shlub  31393  disjiunel  32575  fcoinver  32583  gsumzresunsn  33039  gsumwun  33048  elrgspnsubrunlem1  33214  elrgspnsubrunlem2  33215  elrgspnsubrun  33216  lsmidl  33365  elrspunsn  33393  mxidlprm  33434  qsdrngilem  33458  lindsun  33614  fldgenfldext  33656  evls1fldgencl  33658  fldextrspunlem1  33663  fldextrspunfld  33664  fldextrspunlem2  33665  fldextrspundgdvdslem  33668  fldextrspundgdvds  33669  algextdeglem1  33700  algextdeglem2  33701  algextdeglem3  33702  algextdeglem4  33703  algextdeglem5  33704  rtelextdg2  33710  constrextdg2lem  33731  constrext2chnlem  33733  constrfiss  33734  constrllcllem  33735  constrlccllem  33736  constrcccllem  33737  ordtrestNEW  33904  carsggect  34302  eulerpartlemt  34355  hgt750lemb  34640  hgt750leme  34642  bnj1136  34980  bnj1452  35035  erdszelem8  35178  mclsssvlem  35542  mclsax  35549  mclsind  35550  mthmpps  35562  mclsppslem  35563  topjoin  36346  weiunse  36449  poimirlem32  37639  ftc1anclem7  37686  ftc1anc  37688  prdsbnd  37780  rrnequiv  37822  pclfinN  39887  dochdmj1  41377  djhspss  41393  djhunssN  41396  djhlsmcl  41401  dvh4dimlem  41430  dvhdimlem  41431  lclkrlem2c  41496  lclkrlem2v  41515  mapdh9a  41776  hdmapval0  41820  hdmapval3lemN  41824  hdmap10lem  41826  deg1gprod  42121  dvun  42340  elrfi  42675  cmpfiiin  42678  istopclsd  42681  mzpcompact2lem  42732  eldioph2lem2  42742  eldioph2  42743  rngunsnply  43151  idomsubgmo  43175  omabs2  43314  dfrcl2  43656  iunrelexp0  43684  relexp0a  43698  brtrclfv2  43709  frege77d  43728  frege109d  43739  frege131d  43746  clsk3nimkb  44022  isotone1  44030  ntrclskb  44051  ntrclsk3  44052  ntrclsk13  44053  ntrneixb  44077  ntrneix3  44079  ntrneix13  44081  infxrpnf  45435  pimxrneun  45477  mccllem  45588  limciccioolb  45612  limcicciooub  45628  limcresiooub  45633  limcresioolb  45634  icccncfext  45878  dvnprodlem2  45938  ovolsplit  45979  fourierdlem20  46118  fourierdlem46  46143  fourierdlem48  46145  fourierdlem49  46146  fourierdlem50  46147  fourierdlem51  46148  fourierdlem54  46151  fourierdlem64  46161  fourierdlem76  46173  fourierdlem101  46198  fourierdlem102  46199  fourierdlem103  46200  fourierdlem104  46201  fourierdlem114  46211  sge0resplit  46397  sge0xaddlem1  46424  ismeannd  46458  caragenuncl  46504  omeunle  46507  isomenndlem  46521  hoidmvlelem2  46587  hoidmvlelem3  46588  hoidmvlelem4  46589  perfectALTVlem2  47716  gpgprismgriedgdmss  48036  pgindlem  49697