Theorem unssd 4155

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3912   ⊆ wss 3914

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 3449  df-un 3919  df-ss 3931

This theorem is referenced by:  uneqdifeq  4456  tpssi  4802  sofld  6160  unima  6936  fr3nr  7748  ordsuci  7784  sucexeloniOLD  7786  resf1extb  7910  resf1ext2b  7911  xpord2pred  8124  xpord3pred  8131  frrlem13  8277  naddcllem  8640  ralxpmap  8869  marypha1lem  9384  wemapso2lem  9505  unwf  9763  rankunb  9803  ackbij1lem6  10177  ackbij1lem16  10187  ssfin4  10263  isfin1-3  10339  ttukeylem7  10468  fpwwe2lem12  10595  wuncval2  10700  inar1  10728  un0addcl  12475  un0mulcl  12476  ssfzunsnext  13530  fzosplit  13653  fzouzsplit  13655  hashf1lem1  14420  ccatrn  14554  trclfvlb3  14977  trclun  14980  relexpfld  15015  saddisj  16435  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  lcmfunsnlem2  16610  lcmfun  16615  prmreclem5  16891  4sqlem11  16926  4sqlem19  16934  vdwlem1  16952  vdwlem12  16963  ramub1lem1  16997  ramub1lem2  16998  mrieqvlemd  17590  mreexmrid  17604  mreexexlem2d  17606  mreexexlem3d  17607  mreexexlem4d  17608  acsfiindd  18512  tsrdir  18563  f1omvdco2  19378  symgsssg  19397  symggen  19400  lsmunss  19589  efgsfo  19669  lsptpcl  20885  lspun  20893  lsmsp  20993  lspsolvlem  21052  lspsolv  21053  lsppratlem3  21059  lsppratlem4  21060  islbs3  21065  lbsextlem4  21071  aspval2  21807  evlseu  21990  mhpaddcl  22038  clslp  23035  neitr  23067  ordtuni  23077  ordtbas2  23078  ordtbas  23079  ordtrest  23089  cmpcld  23289  comppfsc  23419  1stckgenlem  23440  1stckgen  23441  ptbasfi  23468  fbun  23727  trfil2  23774  isufil2  23795  ufileu  23806  filufint  23807  fmfnfm  23845  hausflim  23868  flimclslem  23871  fclsfnflim  23914  flimfnfcls  23915  alexsubALTlem3  23936  alexsubALTlem4  23937  tsmsgsum  24026  tsmsres  24031  tsmsxplem1  24040  ustund  24109  trust  24117  ustuqtop1  24129  prdsdsf  24255  prdsxmetlem  24256  prdsmet  24258  prdsbl  24379  prdsxmslem2  24417  restmetu  24458  icccmplem2  24712  rrxmval  25305  rrxmet  25308  rrxdstprj1  25309  ovolunlem1  25398  ovolunnul  25401  nulmbl2  25437  volun  25446  volcn  25507  itgsplitioo  25739  limcvallem  25772  limcdif  25777  ellimc2  25778  limcres  25787  limccnp  25792  limccnp2  25793  limcco  25794  dvreslem  25810  dvres2lem  25811  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  lhop2  25920  dvcnvrelem2  25923  elply2  26101  plyf  26103  elplyr  26106  elplyd  26107  ply1term  26109  ply0  26113  plyeq0lem  26115  plyeq0  26116  plyaddlem  26120  plymullem  26121  dgrlem  26134  coeidlem  26142  plyco  26146  plycj  26183  plycjOLD  26185  aannenlem2  26237  xrlimcnp  26878  perfectlem2  27141  noextend  27578  ssltun1  27720  ssltun2  27721  cutlt  27840  lrrecpred  27851  addsproplem2  27877  addsuniflem  27908  addsbday  27924  negsid  27947  mulsproplem9  28027  ssltmul1  28050  ssltmul2  28051  precsexlem8  28116  precsexlem11  28119  onaddscl  28174  shlej1  31289  shlub  31343  disjiunel  32525  fcoinver  32533  gsumzresunsn  32996  gsumwun  33005  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  elrgspnsubrun  33200  lsmidl  33372  elrspunsn  33400  mxidlprm  33441  qsdrngilem  33465  lindsun  33621  fldgenfldext  33663  evls1fldgencl  33665  fldextrspunlem1  33670  fldextrspunfld  33671  fldextrspunlem2  33672  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  algextdeglem1  33707  algextdeglem2  33708  algextdeglem3  33709  algextdeglem4  33710  algextdeglem5  33711  rtelextdg2  33717  constrextdg2lem  33738  constrext2chnlem  33740  constrfiss  33741  constrllcllem  33742  constrlccllem  33743  constrcccllem  33744  ordtrestNEW  33911  carsggect  34309  eulerpartlemt  34362  hgt750lemb  34647  hgt750leme  34649  bnj1136  34987  bnj1452  35042  erdszelem8  35185  mclsssvlem  35549  mclsax  35556  mclsind  35557  mthmpps  35569  mclsppslem  35570  topjoin  36353  weiunse  36456  poimirlem32  37646  ftc1anclem7  37693  ftc1anc  37695  prdsbnd  37787  rrnequiv  37829  pclfinN  39894  dochdmj1  41384  djhspss  41400  djhunssN  41403  djhlsmcl  41408  dvh4dimlem  41437  dvhdimlem  41438  lclkrlem2c  41503  lclkrlem2v  41522  mapdh9a  41783  hdmapval0  41827  hdmapval3lemN  41831  hdmap10lem  41833  deg1gprod  42128  dvun  42347  elrfi  42682  cmpfiiin  42685  istopclsd  42688  mzpcompact2lem  42739  eldioph2lem2  42749  eldioph2  42750  rngunsnply  43158  idomsubgmo  43182  omabs2  43321  dfrcl2  43663  iunrelexp0  43691  relexp0a  43705  brtrclfv2  43716  frege77d  43735  frege109d  43746  frege131d  43753  clsk3nimkb  44029  isotone1  44037  ntrclskb  44058  ntrclsk3  44059  ntrclsk13  44060  ntrneixb  44084  ntrneix3  44086  ntrneix13  44088  infxrpnf  45442  pimxrneun  45484  mccllem  45595  limciccioolb  45619  limcicciooub  45635  limcresiooub  45640  limcresioolb  45641  icccncfext  45885  dvnprodlem2  45945  ovolsplit  45986  fourierdlem20  46125  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem51  46155  fourierdlem54  46158  fourierdlem64  46168  fourierdlem76  46180  fourierdlem101  46205  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem114  46218  sge0resplit  46404  sge0xaddlem1  46431  ismeannd  46465  caragenuncl  46511  omeunle  46514  isomenndlem  46528  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  perfectALTVlem2  47723  gpgprismgriedgdmss  48043  pgindlem  49704