Theorem unssd 4133

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3888   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907

This theorem is referenced by:  uneqdifeq  4433  tpssi  4782  sofld  6146  unima  6910  fr3nr  7720  ordsuci  7756  resf1extb  7879  resf1ext2b  7880  xpord2pred  8089  xpord3pred  8096  frrlem13  8242  naddcllem  8606  ralxpmap  8838  marypha1lem  9340  wemapso2lem  9461  unwf  9728  rankunb  9768  ackbij1lem6  10140  ackbij1lem16  10150  ssfin4  10226  isfin1-3  10302  ttukeylem7  10431  fpwwe2lem12  10559  wuncval2  10664  inar1  10692  un0addcl  12464  un0mulcl  12465  ssfzunsnext  13517  fzosplit  13641  fzouzsplit  13643  hashf1lem1  14411  ccatrn  14546  trclfvlb3  14967  trclun  14970  relexpfld  15005  saddisj  16428  lcmfunsnlem2lem1  16601  lcmfunsnlem2lem2  16602  lcmfunsnlem2  16603  lcmfun  16608  prmreclem5  16885  4sqlem11  16920  4sqlem19  16928  vdwlem1  16946  vdwlem12  16957  ramub1lem1  16991  ramub1lem2  16992  mrieqvlemd  17589  mreexmrid  17603  mreexexlem2d  17605  mreexexlem3d  17606  mreexexlem4d  17607  acsfiindd  18513  tsrdir  18564  f1omvdco2  19417  symgsssg  19436  symggen  19439  lsmunss  19628  efgsfo  19708  lsptpcl  20968  lspun  20976  lsmsp  21076  lspsolvlem  21135  lspsolv  21136  lsppratlem3  21142  lsppratlem4  21143  islbs3  21148  lbsextlem4  21154  aspval2  21891  evlseu  22074  mhpaddcl  22130  clslp  23126  neitr  23158  ordtuni  23168  ordtbas2  23169  ordtbas  23170  ordtrest  23180  cmpcld  23380  comppfsc  23510  1stckgenlem  23531  1stckgen  23532  ptbasfi  23559  fbun  23818  trfil2  23865  isufil2  23886  ufileu  23897  filufint  23898  fmfnfm  23936  hausflim  23959  flimclslem  23962  fclsfnflim  24005  flimfnfcls  24006  alexsubALTlem3  24027  alexsubALTlem4  24028  tsmsgsum  24117  tsmsres  24122  tsmsxplem1  24131  ustund  24200  trust  24207  ustuqtop1  24219  prdsdsf  24345  prdsxmetlem  24346  prdsmet  24348  prdsbl  24469  prdsxmslem2  24507  restmetu  24548  icccmplem2  24802  rrxmval  25385  rrxmet  25388  rrxdstprj1  25389  ovolunlem1  25477  ovolunnul  25480  nulmbl2  25516  volun  25525  volcn  25586  itgsplitioo  25818  limcvallem  25851  limcdif  25856  ellimc2  25857  limcres  25866  limccnp  25871  limccnp2  25872  limcco  25873  dvreslem  25889  dvres2lem  25890  dvaddbr  25918  dvmulbr  25919  lhop2  25995  dvcnvrelem2  25998  elply2  26174  plyf  26176  elplyr  26179  elplyd  26180  ply1term  26182  ply0  26186  plyeq0lem  26188  plyeq0  26189  plyaddlem  26193  plymullem  26194  dgrlem  26207  coeidlem  26215  plyco  26219  plycj  26255  plycjOLD  26257  aannenlem2  26309  xrlimcnp  26948  perfectlem2  27210  noextend  27647  sltsun1  27797  sltsun2  27798  cutlt  27941  lrrecpred  27953  addsproplem2  27979  addsuniflem  28010  addbday  28027  negsid  28050  mulsproplem9  28133  sltmuls1  28156  sltmuls2  28157  precsexlem8  28223  precsexlem11  28226  onaddscl  28286  bdaypw2n0bndlem  28472  shlej1  31449  shlub  31503  disjiunel  32684  fcoinver  32692  gsumzresunsn  33141  gsumwun  33155  elrgspnsubrunlem1  33326  elrgspnsubrunlem2  33327  elrgspnsubrun  33328  lsmidl  33479  elrspunsn  33507  mxidlprm  33548  qsdrngilem  33572  esplyind  33737  lindsun  33788  fldgenfldext  33831  evls1fldgencl  33833  fldextrspunlem1  33838  fldextrspunfld  33839  fldextrspunlem2  33840  fldextrspundgdvdslem  33843  fldextrspundgdvds  33844  algextdeglem1  33880  algextdeglem2  33881  algextdeglem3  33882  algextdeglem4  33883  algextdeglem5  33884  rtelextdg2  33890  constrextdg2lem  33911  constrext2chnlem  33913  constrfiss  33914  constrllcllem  33915  constrlccllem  33916  constrcccllem  33917  ordtrestNEW  34084  carsggect  34481  eulerpartlemt  34534  hgt750lemb  34819  hgt750leme  34821  bnj1136  35158  bnj1452  35213  erdszelem8  35399  mclsssvlem  35763  mclsax  35770  mclsind  35771  mthmpps  35783  mclsppslem  35784  topjoin  36566  weiunse  36669  poimirlem32  37990  ftc1anclem7  38037  ftc1anc  38039  prdsbnd  38131  rrnequiv  38173  pclfinN  40363  dochdmj1  41853  djhspss  41869  djhunssN  41872  djhlsmcl  41877  dvh4dimlem  41906  dvhdimlem  41907  lclkrlem2c  41972  lclkrlem2v  41991  mapdh9a  42252  hdmapval0  42296  hdmapval3lemN  42300  hdmap10lem  42302  deg1gprod  42596  dvun  42808  elrfi  43143  cmpfiiin  43146  istopclsd  43149  mzpcompact2lem  43200  eldioph2lem2  43210  eldioph2  43211  rngunsnply  43618  idomsubgmo  43642  omabs2  43781  dfrcl2  44122  iunrelexp0  44150  relexp0a  44164  brtrclfv2  44175  frege77d  44194  frege109d  44205  frege131d  44212  clsk3nimkb  44488  isotone1  44496  ntrclskb  44517  ntrclsk3  44518  ntrclsk13  44519  ntrneixb  44543  ntrneix3  44545  ntrneix13  44547  infxrpnf  45895  pimxrneun  45937  mccllem  46048  limciccioolb  46072  limcicciooub  46086  limcresiooub  46091  limcresioolb  46092  icccncfext  46336  dvnprodlem2  46396  ovolsplit  46437  fourierdlem20  46576  fourierdlem46  46601  fourierdlem48  46603  fourierdlem49  46604  fourierdlem50  46605  fourierdlem51  46606  fourierdlem54  46609  fourierdlem64  46619  fourierdlem76  46631  fourierdlem101  46656  fourierdlem102  46657  fourierdlem103  46658  fourierdlem104  46659  fourierdlem114  46669  sge0resplit  46855  sge0xaddlem1  46882  ismeannd  46916  caragenuncl  46962  omeunle  46965  isomenndlem  46979  hoidmvlelem2  47045  hoidmvlelem3  47046  hoidmvlelem4  47047  perfectALTVlem2  48213  gpgprismgriedgdmss  48543  pgindlem  50205