Theorem unssd 4142

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3897   ⊆ wss 3899

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916

This theorem is referenced by:  uneqdifeq  4443  tpssi  4792  sofld  6143  unima  6907  fr3nr  7715  ordsuci  7751  resf1extb  7874  resf1ext2b  7875  xpord2pred  8085  xpord3pred  8092  frrlem13  8238  naddcllem  8602  ralxpmap  8832  marypha1lem  9334  wemapso2lem  9455  unwf  9720  rankunb  9760  ackbij1lem6  10132  ackbij1lem16  10142  ssfin4  10218  isfin1-3  10294  ttukeylem7  10423  fpwwe2lem12  10551  wuncval2  10656  inar1  10684  un0addcl  12432  un0mulcl  12433  ssfzunsnext  13483  fzosplit  13606  fzouzsplit  13608  hashf1lem1  14376  ccatrn  14511  trclfvlb3  14932  trclun  14935  relexpfld  14970  saddisj  16390  lcmfunsnlem2lem1  16563  lcmfunsnlem2lem2  16564  lcmfunsnlem2  16565  lcmfun  16570  prmreclem5  16846  4sqlem11  16881  4sqlem19  16889  vdwlem1  16907  vdwlem12  16918  ramub1lem1  16952  ramub1lem2  16953  mrieqvlemd  17550  mreexmrid  17564  mreexexlem2d  17566  mreexexlem3d  17567  mreexexlem4d  17568  acsfiindd  18474  tsrdir  18525  f1omvdco2  19375  symgsssg  19394  symggen  19397  lsmunss  19586  efgsfo  19666  lsptpcl  20928  lspun  20936  lsmsp  21036  lspsolvlem  21095  lspsolv  21096  lsppratlem3  21102  lsppratlem4  21103  islbs3  21108  lbsextlem4  21114  aspval2  21852  evlseu  22036  mhpaddcl  22092  clslp  23090  neitr  23122  ordtuni  23132  ordtbas2  23133  ordtbas  23134  ordtrest  23144  cmpcld  23344  comppfsc  23474  1stckgenlem  23495  1stckgen  23496  ptbasfi  23523  fbun  23782  trfil2  23829  isufil2  23850  ufileu  23861  filufint  23862  fmfnfm  23900  hausflim  23923  flimclslem  23926  fclsfnflim  23969  flimfnfcls  23970  alexsubALTlem3  23991  alexsubALTlem4  23992  tsmsgsum  24081  tsmsres  24086  tsmsxplem1  24095  ustund  24164  trust  24171  ustuqtop1  24183  prdsdsf  24309  prdsxmetlem  24310  prdsmet  24312  prdsbl  24433  prdsxmslem2  24471  restmetu  24512  icccmplem2  24766  rrxmval  25359  rrxmet  25362  rrxdstprj1  25363  ovolunlem1  25452  ovolunnul  25455  nulmbl2  25491  volun  25500  volcn  25561  itgsplitioo  25793  limcvallem  25826  limcdif  25831  ellimc2  25832  limcres  25841  limccnp  25846  limccnp2  25847  limcco  25848  dvreslem  25864  dvres2lem  25865  dvaddbr  25894  dvmulbr  25895  dvmulbrOLD  25896  lhop2  25974  dvcnvrelem2  25977  elply2  26155  plyf  26157  elplyr  26160  elplyd  26161  ply1term  26163  ply0  26167  plyeq0lem  26169  plyeq0  26170  plyaddlem  26174  plymullem  26175  dgrlem  26188  coeidlem  26196  plyco  26200  plycj  26237  plycjOLD  26239  aannenlem2  26291  xrlimcnp  26932  perfectlem2  27195  noextend  27632  ssltun1  27776  ssltun2  27777  cutlt  27903  lrrecpred  27914  addsproplem2  27940  addsuniflem  27971  addsbday  27987  negsid  28010  mulsproplem9  28093  ssltmul1  28116  ssltmul2  28117  precsexlem8  28182  precsexlem11  28185  onaddscl  28241  bdaypw2n0s  28420  shlej1  31384  shlub  31438  disjiunel  32620  fcoinver  32628  gsumzresunsn  33094  gsumwun  33107  elrgspnsubrunlem1  33278  elrgspnsubrunlem2  33279  elrgspnsubrun  33280  lsmidl  33431  elrspunsn  33459  mxidlprm  33500  qsdrngilem  33524  esplyind  33680  lindsun  33731  fldgenfldext  33774  evls1fldgencl  33776  fldextrspunlem1  33781  fldextrspunfld  33782  fldextrspunlem2  33783  fldextrspundgdvdslem  33786  fldextrspundgdvds  33787  algextdeglem1  33823  algextdeglem2  33824  algextdeglem3  33825  algextdeglem4  33826  algextdeglem5  33827  rtelextdg2  33833  constrextdg2lem  33854  constrext2chnlem  33856  constrfiss  33857  constrllcllem  33858  constrlccllem  33859  constrcccllem  33860  ordtrestNEW  34027  carsggect  34424  eulerpartlemt  34477  hgt750lemb  34762  hgt750leme  34764  bnj1136  35102  bnj1452  35157  erdszelem8  35341  mclsssvlem  35705  mclsax  35712  mclsind  35713  mthmpps  35725  mclsppslem  35726  topjoin  36508  weiunse  36611  poimirlem32  37792  ftc1anclem7  37839  ftc1anc  37841  prdsbnd  37933  rrnequiv  37975  pclfinN  40099  dochdmj1  41589  djhspss  41605  djhunssN  41608  djhlsmcl  41613  dvh4dimlem  41642  dvhdimlem  41643  lclkrlem2c  41708  lclkrlem2v  41727  mapdh9a  41988  hdmapval0  42032  hdmapval3lemN  42036  hdmap10lem  42038  deg1gprod  42333  dvun  42556  elrfi  42878  cmpfiiin  42881  istopclsd  42884  mzpcompact2lem  42935  eldioph2lem2  42945  eldioph2  42946  rngunsnply  43353  idomsubgmo  43377  omabs2  43516  dfrcl2  43857  iunrelexp0  43885  relexp0a  43899  brtrclfv2  43910  frege77d  43929  frege109d  43940  frege131d  43947  clsk3nimkb  44223  isotone1  44231  ntrclskb  44252  ntrclsk3  44253  ntrclsk13  44254  ntrneixb  44278  ntrneix3  44280  ntrneix13  44282  infxrpnf  45632  pimxrneun  45674  mccllem  45785  limciccioolb  45809  limcicciooub  45823  limcresiooub  45828  limcresioolb  45829  icccncfext  46073  dvnprodlem2  46133  ovolsplit  46174  fourierdlem20  46313  fourierdlem46  46338  fourierdlem48  46340  fourierdlem49  46341  fourierdlem50  46342  fourierdlem51  46343  fourierdlem54  46346  fourierdlem64  46356  fourierdlem76  46368  fourierdlem101  46393  fourierdlem102  46394  fourierdlem103  46395  fourierdlem104  46396  fourierdlem114  46406  sge0resplit  46592  sge0xaddlem1  46619  ismeannd  46653  caragenuncl  46699  omeunle  46702  isomenndlem  46716  hoidmvlelem2  46782  hoidmvlelem3  46783  hoidmvlelem4  46784  perfectALTVlem2  47910  gpgprismgriedgdmss  48240  pgindlem  49902