Theorem unssd 4146

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3901   ⊆ wss 3903

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920

This theorem is referenced by:  uneqdifeq  4447  tpssi  4796  sofld  6153  unima  6917  fr3nr  7727  ordsuci  7763  resf1extb  7886  resf1ext2b  7887  xpord2pred  8097  xpord3pred  8104  frrlem13  8250  naddcllem  8614  ralxpmap  8846  marypha1lem  9348  wemapso2lem  9469  unwf  9734  rankunb  9774  ackbij1lem6  10146  ackbij1lem16  10156  ssfin4  10232  isfin1-3  10308  ttukeylem7  10437  fpwwe2lem12  10565  wuncval2  10670  inar1  10698  un0addcl  12446  un0mulcl  12447  ssfzunsnext  13497  fzosplit  13620  fzouzsplit  13622  hashf1lem1  14390  ccatrn  14525  trclfvlb3  14946  trclun  14949  relexpfld  14984  saddisj  16404  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  lcmfunsnlem2  16579  lcmfun  16584  prmreclem5  16860  4sqlem11  16895  4sqlem19  16903  vdwlem1  16921  vdwlem12  16932  ramub1lem1  16966  ramub1lem2  16967  mrieqvlemd  17564  mreexmrid  17578  mreexexlem2d  17580  mreexexlem3d  17581  mreexexlem4d  17582  acsfiindd  18488  tsrdir  18539  f1omvdco2  19389  symgsssg  19408  symggen  19411  lsmunss  19600  efgsfo  19680  lsptpcl  20942  lspun  20950  lsmsp  21050  lspsolvlem  21109  lspsolv  21110  lsppratlem3  21116  lsppratlem4  21117  islbs3  21122  lbsextlem4  21128  aspval2  21866  evlseu  22050  mhpaddcl  22106  clslp  23104  neitr  23136  ordtuni  23146  ordtbas2  23147  ordtbas  23148  ordtrest  23158  cmpcld  23358  comppfsc  23488  1stckgenlem  23509  1stckgen  23510  ptbasfi  23537  fbun  23796  trfil2  23843  isufil2  23864  ufileu  23875  filufint  23876  fmfnfm  23914  hausflim  23937  flimclslem  23940  fclsfnflim  23983  flimfnfcls  23984  alexsubALTlem3  24005  alexsubALTlem4  24006  tsmsgsum  24095  tsmsres  24100  tsmsxplem1  24109  ustund  24178  trust  24185  ustuqtop1  24197  prdsdsf  24323  prdsxmetlem  24324  prdsmet  24326  prdsbl  24447  prdsxmslem2  24485  restmetu  24526  icccmplem2  24780  rrxmval  25373  rrxmet  25376  rrxdstprj1  25377  ovolunlem1  25466  ovolunnul  25469  nulmbl2  25505  volun  25514  volcn  25575  itgsplitioo  25807  limcvallem  25840  limcdif  25845  ellimc2  25846  limcres  25855  limccnp  25860  limccnp2  25861  limcco  25862  dvreslem  25878  dvres2lem  25879  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  lhop2  25988  dvcnvrelem2  25991  elply2  26169  plyf  26171  elplyr  26174  elplyd  26175  ply1term  26177  ply0  26181  plyeq0lem  26183  plyeq0  26184  plyaddlem  26188  plymullem  26189  dgrlem  26202  coeidlem  26210  plyco  26214  plycj  26251  plycjOLD  26253  aannenlem2  26305  xrlimcnp  26946  perfectlem2  27209  noextend  27646  sltsun1  27796  sltsun2  27797  cutlt  27940  lrrecpred  27952  addsproplem2  27978  addsuniflem  28009  addbday  28026  negsid  28049  mulsproplem9  28132  sltmuls1  28155  sltmuls2  28156  precsexlem8  28222  precsexlem11  28225  onaddscl  28285  bdaypw2n0bndlem  28471  shlej1  31448  shlub  31502  disjiunel  32683  fcoinver  32691  gsumzresunsn  33156  gsumwun  33170  elrgspnsubrunlem1  33341  elrgspnsubrunlem2  33342  elrgspnsubrun  33343  lsmidl  33494  elrspunsn  33522  mxidlprm  33563  qsdrngilem  33587  esplyind  33752  lindsun  33803  fldgenfldext  33846  evls1fldgencl  33848  fldextrspunlem1  33853  fldextrspunfld  33854  fldextrspunlem2  33855  fldextrspundgdvdslem  33858  fldextrspundgdvds  33859  algextdeglem1  33895  algextdeglem2  33896  algextdeglem3  33897  algextdeglem4  33898  algextdeglem5  33899  rtelextdg2  33905  constrextdg2lem  33926  constrext2chnlem  33928  constrfiss  33929  constrllcllem  33930  constrlccllem  33931  constrcccllem  33932  ordtrestNEW  34099  carsggect  34496  eulerpartlemt  34549  hgt750lemb  34834  hgt750leme  34836  bnj1136  35173  bnj1452  35228  erdszelem8  35414  mclsssvlem  35778  mclsax  35785  mclsind  35786  mthmpps  35798  mclsppslem  35799  topjoin  36581  weiunse  36684  poimirlem32  37903  ftc1anclem7  37950  ftc1anc  37952  prdsbnd  38044  rrnequiv  38086  pclfinN  40276  dochdmj1  41766  djhspss  41782  djhunssN  41785  djhlsmcl  41790  dvh4dimlem  41819  dvhdimlem  41820  lclkrlem2c  41885  lclkrlem2v  41904  mapdh9a  42165  hdmapval0  42209  hdmapval3lemN  42213  hdmap10lem  42215  deg1gprod  42510  dvun  42729  elrfi  43051  cmpfiiin  43054  istopclsd  43057  mzpcompact2lem  43108  eldioph2lem2  43118  eldioph2  43119  rngunsnply  43526  idomsubgmo  43550  omabs2  43689  dfrcl2  44030  iunrelexp0  44058  relexp0a  44072  brtrclfv2  44083  frege77d  44102  frege109d  44113  frege131d  44120  clsk3nimkb  44396  isotone1  44404  ntrclskb  44425  ntrclsk3  44426  ntrclsk13  44427  ntrneixb  44451  ntrneix3  44453  ntrneix13  44455  infxrpnf  45804  pimxrneun  45846  mccllem  45957  limciccioolb  45981  limcicciooub  45995  limcresiooub  46000  limcresioolb  46001  icccncfext  46245  dvnprodlem2  46305  ovolsplit  46346  fourierdlem20  46485  fourierdlem46  46510  fourierdlem48  46512  fourierdlem49  46513  fourierdlem50  46514  fourierdlem51  46515  fourierdlem54  46518  fourierdlem64  46528  fourierdlem76  46540  fourierdlem101  46565  fourierdlem102  46566  fourierdlem103  46567  fourierdlem104  46568  fourierdlem114  46578  sge0resplit  46764  sge0xaddlem1  46791  ismeannd  46825  caragenuncl  46871  omeunle  46874  isomenndlem  46888  hoidmvlelem2  46954  hoidmvlelem3  46955  hoidmvlelem4  46956  perfectALTVlem2  48082  gpgprismgriedgdmss  48412  pgindlem  50074