Theorem unssd 4201

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3960   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979

This theorem is referenced by:  uneqdifeq  4498  tpssi  4842  sofld  6208  unima  6983  fr3nr  7790  ordsuci  7827  sucexeloniOLD  7829  suceloniOLD  7831  xpord2pred  8168  xpord3pred  8175  frrlem13  8321  naddcllem  8712  ralxpmap  8934  marypha1lem  9470  wemapso2lem  9589  unwf  9847  rankunb  9887  ackbij1lem6  10261  ackbij1lem16  10271  ssfin4  10347  isfin1-3  10423  ttukeylem7  10552  fpwwe2lem12  10679  wuncval2  10784  inar1  10812  un0addcl  12556  un0mulcl  12557  ssfzunsnext  13605  fzosplit  13728  fzouzsplit  13730  hashf1lem1  14490  ccatrn  14623  trclfvlb3  15046  trclun  15049  relexpfld  15084  saddisj  16498  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  lcmfunsnlem2  16673  lcmfun  16678  prmreclem5  16953  4sqlem11  16988  4sqlem19  16996  vdwlem1  17014  vdwlem12  17025  ramub1lem1  17059  ramub1lem2  17060  mrieqvlemd  17673  mreexmrid  17687  mreexexlem2d  17689  mreexexlem3d  17690  mreexexlem4d  17691  acsfiindd  18610  tsrdir  18661  f1omvdco2  19480  symgsssg  19499  symggen  19502  lsmunss  19691  efgsfo  19771  lsptpcl  20994  lspun  21002  lsmsp  21102  lspsolvlem  21161  lspsolv  21162  lsppratlem3  21168  lsppratlem4  21169  islbs3  21174  lbsextlem4  21180  aspval2  21935  evlseu  22124  mhpaddcl  22172  clslp  23171  neitr  23203  ordtuni  23213  ordtbas2  23214  ordtbas  23215  ordtrest  23225  cmpcld  23425  comppfsc  23555  1stckgenlem  23576  1stckgen  23577  ptbasfi  23604  fbun  23863  trfil2  23910  isufil2  23931  ufileu  23942  filufint  23943  fmfnfm  23981  hausflim  24004  flimclslem  24007  fclsfnflim  24050  flimfnfcls  24051  alexsubALTlem3  24072  alexsubALTlem4  24073  tsmsgsum  24162  tsmsres  24167  tsmsxplem1  24176  ustund  24245  trust  24253  ustuqtop1  24265  prdsdsf  24392  prdsxmetlem  24393  prdsmet  24395  prdsbl  24519  prdsxmslem2  24557  restmetu  24598  icccmplem2  24858  rrxmval  25452  rrxmet  25455  rrxdstprj1  25456  ovolunlem1  25545  ovolunnul  25548  nulmbl2  25584  volun  25593  volcn  25654  itgsplitioo  25887  limcvallem  25920  limcdif  25925  ellimc2  25926  limcres  25935  limccnp  25940  limccnp2  25941  limcco  25942  dvreslem  25958  dvres2lem  25959  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  lhop2  26068  dvcnvrelem2  26071  elply2  26249  plyf  26251  elplyr  26254  elplyd  26255  ply1term  26257  ply0  26261  plyeq0lem  26263  plyeq0  26264  plyaddlem  26268  plymullem  26269  dgrlem  26282  coeidlem  26290  plyco  26294  plycj  26331  plycjOLD  26333  aannenlem2  26385  xrlimcnp  27025  perfectlem2  27288  noextend  27725  ssltun1  27867  ssltun2  27868  cutlt  27980  lrrecpred  27991  addsproplem2  28017  addsuniflem  28048  addsbday  28064  negsid  28087  mulsproplem9  28164  ssltmul1  28187  ssltmul2  28188  precsexlem8  28252  precsexlem11  28255  onaddscl  28300  shlej1  31388  shlub  31442  disjiunel  32615  fcoinver  32623  gsumzresunsn  33041  gsumwun  33050  lsmidl  33408  elrspunsn  33436  mxidlprm  33477  qsdrngilem  33501  lindsun  33652  fldgenfldext  33692  evls1fldgencl  33694  algextdeglem1  33722  algextdeglem2  33723  algextdeglem3  33724  algextdeglem4  33725  algextdeglem5  33726  rtelextdg2  33732  ordtrestNEW  33881  carsggect  34299  eulerpartlemt  34352  hgt750lemb  34649  hgt750leme  34651  bnj1136  34989  bnj1452  35044  erdszelem8  35182  mclsssvlem  35546  mclsax  35553  mclsind  35554  mthmpps  35566  mclsppslem  35567  topjoin  36347  weiunse  36450  poimirlem32  37638  ftc1anclem7  37685  ftc1anc  37687  prdsbnd  37779  rrnequiv  37821  pclfinN  39882  dochdmj1  41372  djhspss  41388  djhunssN  41391  djhlsmcl  41396  dvh4dimlem  41425  dvhdimlem  41426  lclkrlem2c  41491  lclkrlem2v  41510  mapdh9a  41771  hdmapval0  41815  hdmapval3lemN  41819  hdmap10lem  41821  deg1gprod  42121  dvun  42367  elrfi  42681  cmpfiiin  42684  istopclsd  42687  mzpcompact2lem  42738  eldioph2lem2  42748  eldioph2  42749  rngunsnply  43157  idomsubgmo  43181  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  45395  pimxrneun  45438  mccllem  45552  limciccioolb  45576  limcicciooub  45592  limcresiooub  45597  limcresioolb  45598  icccncfext  45842  dvnprodlem2  45902  ovolsplit  45943  fourierdlem20  46082  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem51  46112  fourierdlem54  46115  fourierdlem64  46125  fourierdlem76  46137  fourierdlem101  46162  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem114  46175  sge0resplit  46361  sge0xaddlem1  46388  ismeannd  46422  caragenuncl  46468  omeunle  46471  isomenndlem  46485  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  perfectALTVlem2  47646  pgindlem  48945