Theorem unssd 4172

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3929   ⊆ wss 3931

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-ss 3948

This theorem is referenced by:  uneqdifeq  4473  tpssi  4819  sofld  6181  unima  6959  fr3nr  7771  ordsuci  7807  sucexeloniOLD  7809  suceloniOLD  7811  resf1extb  7935  resf1ext2b  7936  xpord2pred  8149  xpord3pred  8156  frrlem13  8302  naddcllem  8693  ralxpmap  8915  marypha1lem  9450  wemapso2lem  9571  unwf  9829  rankunb  9869  ackbij1lem6  10243  ackbij1lem16  10253  ssfin4  10329  isfin1-3  10405  ttukeylem7  10534  fpwwe2lem12  10661  wuncval2  10766  inar1  10794  un0addcl  12539  un0mulcl  12540  ssfzunsnext  13591  fzosplit  13714  fzouzsplit  13716  hashf1lem1  14478  ccatrn  14612  trclfvlb3  15035  trclun  15038  relexpfld  15073  saddisj  16489  lcmfunsnlem2lem1  16662  lcmfunsnlem2lem2  16663  lcmfunsnlem2  16664  lcmfun  16669  prmreclem5  16945  4sqlem11  16980  4sqlem19  16988  vdwlem1  17006  vdwlem12  17017  ramub1lem1  17051  ramub1lem2  17052  mrieqvlemd  17646  mreexmrid  17660  mreexexlem2d  17662  mreexexlem3d  17663  mreexexlem4d  17664  acsfiindd  18568  tsrdir  18619  f1omvdco2  19434  symgsssg  19453  symggen  19456  lsmunss  19645  efgsfo  19725  lsptpcl  20941  lspun  20949  lsmsp  21049  lspsolvlem  21108  lspsolv  21109  lsppratlem3  21115  lsppratlem4  21116  islbs3  21121  lbsextlem4  21127  aspval2  21863  evlseu  22046  mhpaddcl  22094  clslp  23091  neitr  23123  ordtuni  23133  ordtbas2  23134  ordtbas  23135  ordtrest  23145  cmpcld  23345  comppfsc  23475  1stckgenlem  23496  1stckgen  23497  ptbasfi  23524  fbun  23783  trfil2  23830  isufil2  23851  ufileu  23862  filufint  23863  fmfnfm  23901  hausflim  23924  flimclslem  23927  fclsfnflim  23970  flimfnfcls  23971  alexsubALTlem3  23992  alexsubALTlem4  23993  tsmsgsum  24082  tsmsres  24087  tsmsxplem1  24096  ustund  24165  trust  24173  ustuqtop1  24185  prdsdsf  24311  prdsxmetlem  24312  prdsmet  24314  prdsbl  24435  prdsxmslem2  24473  restmetu  24514  icccmplem2  24768  rrxmval  25362  rrxmet  25365  rrxdstprj1  25366  ovolunlem1  25455  ovolunnul  25458  nulmbl2  25494  volun  25503  volcn  25564  itgsplitioo  25796  limcvallem  25829  limcdif  25834  ellimc2  25835  limcres  25844  limccnp  25849  limccnp2  25850  limcco  25851  dvreslem  25867  dvres2lem  25868  dvaddbr  25897  dvmulbr  25898  dvmulbrOLD  25899  lhop2  25977  dvcnvrelem2  25980  elply2  26158  plyf  26160  elplyr  26163  elplyd  26164  ply1term  26166  ply0  26170  plyeq0lem  26172  plyeq0  26173  plyaddlem  26177  plymullem  26178  dgrlem  26191  coeidlem  26199  plyco  26203  plycj  26240  plycjOLD  26242  aannenlem2  26294  xrlimcnp  26935  perfectlem2  27198  noextend  27635  ssltun1  27777  ssltun2  27778  cutlt  27897  lrrecpred  27908  addsproplem2  27934  addsuniflem  27965  addsbday  27981  negsid  28004  mulsproplem9  28084  ssltmul1  28107  ssltmul2  28108  precsexlem8  28173  precsexlem11  28176  onaddscl  28231  shlej1  31346  shlub  31400  disjiunel  32582  fcoinver  32590  gsumzresunsn  33055  gsumwun  33064  elrgspnsubrunlem1  33247  elrgspnsubrunlem2  33248  elrgspnsubrun  33249  lsmidl  33421  elrspunsn  33449  mxidlprm  33490  qsdrngilem  33514  lindsun  33670  fldgenfldext  33714  evls1fldgencl  33716  fldextrspunlem1  33721  fldextrspunfld  33722  fldextrspunlem2  33723  fldextrspundgdvdslem  33726  fldextrspundgdvds  33727  algextdeglem1  33756  algextdeglem2  33757  algextdeglem3  33758  algextdeglem4  33759  algextdeglem5  33760  rtelextdg2  33766  constrextdg2lem  33787  constrext2chnlem  33789  constrfiss  33790  constrllcllem  33791  constrlccllem  33792  constrcccllem  33793  ordtrestNEW  33957  carsggect  34355  eulerpartlemt  34408  hgt750lemb  34693  hgt750leme  34695  bnj1136  35033  bnj1452  35088  erdszelem8  35225  mclsssvlem  35589  mclsax  35596  mclsind  35597  mthmpps  35609  mclsppslem  35610  topjoin  36388  weiunse  36491  poimirlem32  37681  ftc1anclem7  37728  ftc1anc  37730  prdsbnd  37822  rrnequiv  37864  pclfinN  39924  dochdmj1  41414  djhspss  41430  djhunssN  41433  djhlsmcl  41438  dvh4dimlem  41467  dvhdimlem  41468  lclkrlem2c  41533  lclkrlem2v  41552  mapdh9a  41813  hdmapval0  41857  hdmapval3lemN  41861  hdmap10lem  41863  deg1gprod  42158  dvun  42377  elrfi  42692  cmpfiiin  42695  istopclsd  42698  mzpcompact2lem  42749  eldioph2lem2  42759  eldioph2  42760  rngunsnply  43168  idomsubgmo  43192  omabs2  43331  dfrcl2  43673  iunrelexp0  43701  relexp0a  43715  brtrclfv2  43726  frege77d  43745  frege109d  43756  frege131d  43763  clsk3nimkb  44039  isotone1  44047  ntrclskb  44068  ntrclsk3  44069  ntrclsk13  44070  ntrneixb  44094  ntrneix3  44096  ntrneix13  44098  infxrpnf  45453  pimxrneun  45495  mccllem  45606  limciccioolb  45630  limcicciooub  45646  limcresiooub  45651  limcresioolb  45652  icccncfext  45896  dvnprodlem2  45956  ovolsplit  45997  fourierdlem20  46136  fourierdlem46  46161  fourierdlem48  46163  fourierdlem49  46164  fourierdlem50  46165  fourierdlem51  46166  fourierdlem54  46169  fourierdlem64  46179  fourierdlem76  46191  fourierdlem101  46216  fourierdlem102  46217  fourierdlem103  46218  fourierdlem104  46219  fourierdlem114  46229  sge0resplit  46415  sge0xaddlem1  46442  ismeannd  46476  caragenuncl  46522  omeunle  46525  isomenndlem  46539  hoidmvlelem2  46605  hoidmvlelem3  46606  hoidmvlelem4  46607  perfectALTVlem2  47716  gpgprismgriedgdmss  48036  pgindlem  49559