Theorem unssd 4162

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

Syntax hints:   → wi 4   ∧ wa 398   ∪ cun 3934   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952

This theorem is referenced by:  uneqdifeq  4438  tpssi  4769  sofld  6044  unima  6739  fr3nr  7494  suceloni  7528  ralxpmap  8460  marypha1lem  8897  wemapso2lem  9016  unwf  9239  rankunb  9279  ackbij1lem6  9647  ackbij1lem16  9657  ssfin4  9732  isfin1-3  9808  ttukeylem7  9937  fpwwe2lem13  10064  wuncval2  10169  inar1  10197  un0addcl  11931  un0mulcl  11932  ssfzunsnext  12953  fzosplit  13071  fzouzsplit  13073  hashf1lem1  13814  ccatrn  13943  trclfvlb3  14371  trclun  14374  relexpfld  14408  saddisj  15814  lcmfunsnlem2lem1  15982  lcmfunsnlem2lem2  15983  lcmfunsnlem2  15984  lcmfun  15989  prmreclem5  16256  4sqlem11  16291  4sqlem19  16299  vdwlem1  16317  vdwlem12  16328  ramub1lem1  16362  ramub1lem2  16363  mrieqvlemd  16900  mreexmrid  16914  mreexexlem2d  16916  mreexexlem3d  16917  mreexexlem4d  16918  acsfiindd  17787  tsrdir  17848  f1omvdco2  18576  symgsssg  18595  symggen  18598  lsmunss  18784  efgsfo  18865  lsptpcl  19751  lspun  19759  lsmsp  19858  lspsolvlem  19914  lspsolv  19915  lsppratlem3  19921  lsppratlem4  19922  islbs3  19927  lbsextlem4  19933  aspval2  20127  evlseu  20296  mhpaddcl  20338  clslp  21756  neitr  21788  ordtuni  21798  ordtbas2  21799  ordtbas  21800  ordtrest  21810  cmpcld  22010  comppfsc  22140  1stckgenlem  22161  1stckgen  22162  ptbasfi  22189  fbun  22448  trfil2  22495  isufil2  22516  ufileu  22527  filufint  22528  fmfnfm  22566  hausflim  22589  flimclslem  22592  fclsfnflim  22635  flimfnfcls  22636  alexsubALTlem3  22657  alexsubALTlem4  22658  tsmsgsum  22747  tsmsres  22752  tsmsxplem1  22761  ustund  22830  trust  22838  ustuqtop1  22850  prdsdsf  22977  prdsxmetlem  22978  prdsmet  22980  prdsbl  23101  prdsxmslem2  23139  restmetu  23180  icccmplem2  23431  rrxmval  24008  rrxmet  24011  rrxdstprj1  24012  ovolunlem1  24098  ovolunnul  24101  nulmbl2  24137  volun  24146  volcn  24207  itgsplitioo  24438  limcvallem  24469  limcdif  24474  ellimc2  24475  limcres  24484  limccnp  24489  limccnp2  24490  limcco  24491  dvreslem  24507  dvres2lem  24508  dvaddbr  24535  dvmulbr  24536  lhop2  24612  dvcnvrelem2  24615  elply2  24786  plyf  24788  elplyr  24791  elplyd  24792  ply1term  24794  ply0  24798  plyeq0lem  24800  plyeq0  24801  plyaddlem  24805  plymullem  24806  dgrlem  24819  coeidlem  24827  plyco  24831  plycj  24867  aannenlem2  24918  xrlimcnp  25546  perfectlem2  25806  shlej1  29137  shlub  29191  disjiunel  30346  fcoinver  30357  gsumzresunsn  30691  lsmidl  30951  mxidlprm  30977  lindsun  31021  ordtrestNEW  31164  carsggect  31576  eulerpartlemt  31629  hgt750lemb  31927  hgt750leme  31929  bnj1136  32269  bnj1452  32324  erdszelem8  32445  mclsssvlem  32809  mclsax  32816  mclsind  32817  mthmpps  32829  mclsppslem  32830  dftrpred3g  33072  frrlem13  33135  noextend  33173  ssltun1  33269  ssltun2  33270  topjoin  33713  poimirlem32  34939  ftc1anclem7  34988  ftc1anc  34990  prdsbnd  35086  rrnequiv  35128  pclfinN  37051  dochdmj1  38541  djhspss  38557  djhunssN  38560  djhlsmcl  38565  dvh4dimlem  38594  dvhdimlem  38595  lclkrlem2c  38660  lclkrlem2v  38679  mapdh9a  38940  hdmapval0  38984  hdmapval3lemN  38988  hdmap10lem  38990  elrfi  39340  cmpfiiin  39343  istopclsd  39346  mzpcompact2lem  39397  eldioph2lem2  39407  eldioph2  39408  rngunsnply  39822  idomsubgmo  39847  dfrcl2  40068  iunrelexp0  40096  relexp0a  40110  brtrclfv2  40121  frege77d  40140  frege109d  40151  frege131d  40158  clsk3nimkb  40439  isotone1  40447  ntrclskb  40468  ntrclsk3  40469  ntrclsk13  40470  ntrneixb  40494  ntrneix3  40496  ntrneix13  40498  infxrpnf  41770  mccllem  41927  limciccioolb  41951  limcicciooub  41967  limcresiooub  41972  limcresioolb  41973  icccncfext  42219  dvnprodlem2  42281  ovolsplit  42322  fourierdlem20  42461  fourierdlem46  42486  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem51  42491  fourierdlem54  42494  fourierdlem64  42504  fourierdlem76  42516  fourierdlem101  42541  fourierdlem102  42542  fourierdlem103  42543  fourierdlem104  42544  fourierdlem114  42554  sge0resplit  42737  sge0xaddlem1  42764  ismeannd  42798  caragenuncl  42844  omeunle  42847  isomenndlem  42861  hoidmvlelem2  42927  hoidmvlelem3  42928  hoidmvlelem4  42929  perfectALTVlem2  43936