Theorem unssd 4144

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

Syntax hints:   → wi 4   ∧ wa 399   ∪ cun 3902   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921

This theorem is referenced by:  uneqdifeq  4446  tpssi  4796  sofld  6173  unima  6942  fr3nr  7755  ordsuci  7791  resf1extb  7915  resf1ext2b  7916  xpord2pred  8125  xpord3pred  8132  frrlem13  8279  naddcllem  8646  ralxpmap  8878  marypha1lem  9379  wemapso2lem  9500  unwf  9768  rankunb  9808  ackbij1lem6  10180  ackbij1lem16  10190  ssfin4  10267  isfin1-3  10343  ttukeylem7  10472  fpwwe2lem12  10600  wuncval2  10705  inar1  10733  un0addcl  12514  un0mulcl  12515  ssfzunsnext  13574  fzosplit  13698  fzouzsplit  13700  hashf1lem1  14468  ccatrn  14603  trclfvlb3  15024  trclun  15027  relexpfld  15062  saddisj  16499  lcmfunsnlem2lem1  16672  lcmfunsnlem2lem2  16673  lcmfunsnlem2  16674  lcmfun  16679  prmreclem5  16956  4sqlem11  16991  4sqlem19  16999  vdwlem1  17017  vdwlem12  17028  ramub1lem1  17062  ramub1lem2  17063  mrieqvlemd  17661  mreexmrid  17675  mreexexlem2d  17677  mreexexlem3d  17678  mreexexlem4d  17679  acsfiindd  18585  tsrdir  18636  f1omvdco2  19488  symgsssg  19507  symggen  19510  lsmunss  19699  efgsfo  19779  lsptpcl  21046  lspun  21054  lsmsp  21153  lspsolvlem  21212  lspsolv  21213  lsppratlem3  21219  lsppratlem4  21220  islbs3  21225  lbsextlem4  21231  aspval2  21950  evlseu  22136  mhpaddcl  22216  clslp  23208  neitr  23240  ordtuni  23250  ordtbas2  23251  ordtbas  23252  ordtrest  23262  cmpcld  23462  comppfsc  23592  1stckgenlem  23613  1stckgen  23614  ptbasfi  23641  fbun  23900  trfil2  23947  isufil2  23968  ufileu  23979  filufint  23980  fmfnfm  24018  hausflim  24041  flimclslem  24044  fclsfnflim  24087  flimfnfcls  24088  alexsubALTlem3  24109  alexsubALTlem4  24110  tsmsgsum  24199  tsmsres  24204  tsmsxplem1  24213  ustund  24282  trust  24289  ustuqtop1  24301  prdsdsf  24427  prdsxmetlem  24428  prdsmet  24430  prdsbl  24551  prdsxmslem2  24589  restmetu  24630  icccmplem2  24884  rrxmval  25467  rrxmet  25470  rrxdstprj1  25471  ovolunlem1  25559  ovolunnul  25562  nulmbl2  25598  volun  25607  volcn  25668  itgsplitioo  25900  limcvallem  25933  limcdif  25938  ellimc2  25939  limcres  25948  limccnp  25953  limccnp2  25954  limcco  25955  dvreslem  25971  dvres2lem  25972  dvaddbr  26000  dvmulbr  26001  lhop2  26077  dvcnvrelem2  26080  elply2  26256  plyf  26258  elplyr  26261  elplyd  26262  ply1term  26264  ply0  26268  plyeq0lem  26270  plyeq0  26271  plyaddlem  26275  plymullem  26276  dgrlem  26289  coeidlem  26297  plyco  26301  plycj  26337  plycjOLD  26339  aannenlem2  26393  xrlimcnp  27033  perfectlem2  27294  noextend  27730  sltsun1  27881  sltsun2  27882  cutlt  28025  lrrecpred  28037  addsproplem2  28063  addsuniflem  28094  addbday  28111  negsid  28134  mulsproplem9  28217  sltmuls1  28240  sltmuls2  28241  precsexlem8  28307  precsexlem11  28310  onaddscl  28370  bdaypw2n0bndlem  28556  shlej1  31563  shlub  31617  disjiunel  32796  fcoinver  32804  gsumzresunsn  33242  gsumwun  33256  elrgspnsubrunlem1  33428  elrgspnsubrunlem2  33429  elrgspnsubrun  33430  lsmidl  33587  elrspunsn  33615  mxidlprm  33658  qsdrngilem  33682  esplyind  33872  lindsun  33922  fldgenfldext  33965  evls1fldgencl  33967  fldextrspunlem1  33972  fldextrspunfld  33973  fldextrspunlem2  33974  fldextrspundgdvdslem  33977  fldextrspundgdvds  33978  algextdeglem1  34014  algextdeglem2  34015  algextdeglem3  34016  algextdeglem4  34017  algextdeglem5  34018  rtelextdg2  34024  constrextdg2lem  34045  constrext2chnlem  34047  constrfiss  34048  constrllcllem  34049  constrlccllem  34050  constrcccllem  34051  ordtrestNEW  34218  carsggect  34615  eulerpartlemt  34668  hgt750lemb  34950  hgt750leme  34952  bnj1136  35292  bnj1452  35347  erdszelem8  35548  mclsssvlem  35912  mclsax  35919  mclsind  35920  mthmpps  35932  mclsppslem  35933  topjoin  36725  weiunse  36828  poimirlem32  38151  ftc1anclem7  38198  ftc1anc  38200  prdsbnd  38292  rrnequiv  38334  pclfinN  40524  dochdmj1  42014  djhspss  42030  djhunssN  42033  djhlsmcl  42038  dvh4dimlem  42067  dvhdimlem  42068  lclkrlem2c  42133  lclkrlem2v  42152  mapdh9a  42413  hdmapval0  42457  hdmapval3lemN  42461  hdmap10lem  42463  deg1gprod  42757  dvun  42968  elrfi  43275  cmpfiiin  43278  istopclsd  43281  mzpcompact2lem  43332  eldioph2lem2  43342  eldioph2  43343  rngunsnply  43746  idomsubgmo  43770  omabs2  43909  dfrcl2  44250  iunrelexp0  44278  relexp0a  44292  brtrclfv2  44303  frege77d  44322  frege109d  44333  frege131d  44340  clsk3nimkb  44616  isotone1  44624  ntrclskb  44645  ntrclsk3  44646  ntrclsk13  44647  ntrneixb  44671  ntrneix3  44673  ntrneix13  44675  infxrpnf  46020  pimxrneun  46062  mccllem  46173  limciccioolb  46197  limcicciooub  46211  limcresiooub  46216  limcresioolb  46217  icccncfext  46461  dvnprodlem2  46521  ovolsplit  46562  fourierdlem20  46701  fourierdlem46  46726  fourierdlem48  46728  fourierdlem49  46729  fourierdlem50  46730  fourierdlem51  46731  fourierdlem54  46734  fourierdlem64  46744  fourierdlem76  46756  fourierdlem101  46781  fourierdlem102  46782  fourierdlem103  46783  fourierdlem104  46784  fourierdlem114  46794  sge0resplit  46980  sge0xaddlem1  47007  ismeannd  47041  caragenuncl  47087  omeunle  47090  isomenndlem  47104  hoidmvlelem2  47170  hoidmvlelem3  47171  hoidmvlelem4  47172  perfectALTVlem2  48344  gpgprismgriedgdmss  48674  pgindlem  50336