Theorem unssd 4145

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∪ cun 3904   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923

This theorem is used by:  uneqdifeq  4455  tpssi  4805  sofld  6187  unima  6960  fr3nr  7777  ordsuci  7813  resf1extb  7937  resf1ext2b  7938  xpord2pred  8147  xpord3pred  8154  frrlem13  8301  naddcllem  8668  ralxpmap  8900  marypha1lem  9400  wemapso2lem  9521  unwf  9789  rankunb  9829  ackbij1lem6  10223  ackbij1lem16  10233  ssfin4  10309  isfin1-3  10385  ttukeylem7  10514  fpwwe2lem12  10642  wuncval2  10747  inar1  10775  un0addcl  12552  un0mulcl  12553  ssfzunsnext  13614  fzosplit  13738  fzouzsplit  13740  hashf1lem1  14510  ccatrn  14645  trclfvlb3  15072  trclun  15075  relexpfld  15110  saddisj  16545  lcmfunsnlem2lem1  16718  lcmfunsnlem2lem2  16719  lcmfunsnlem2  16720  lcmfun  16725  prmreclem5  17002  4sqlem11  17037  4sqlem19  17045  vdwlem1  17063  vdwlem12  17074  ramub1lem1  17108  ramub1lem2  17109  mrieqvlemd  17707  mreexmrid  17721  mreexexlem2d  17723  mreexexlem3d  17724  mreexexlem4d  17725  acsfiindd  18631  tsrdir  18682  f1omvdco2  19562  symgsssg  19581  symggen  19584  lsmunss  19773  efgsfo  19853  lsptpcl  21150  lspun  21158  lsmsp  21257  lspsolvlem  21316  lspsolv  21317  lsppratlem3  21323  lsppratlem4  21324  islbs3  21329  lbsextlem4  21335  lsmidl  21434  aspval2  22098  evlseu  22284  mhpaddcl  22364  clslp  23355  neitr  23387  ordtuni  23397  ordtbas2  23398  ordtbas  23399  ordtrest  23409  cmpcld  23609  comppfsc  23740  1stckgenlem  23761  1stckgen  23762  ptbasfi  23789  fbun  24048  trfil2  24095  isufil2  24116  ufileu  24127  filufint  24128  fmfnfm  24166  hausflim  24189  flimclslem  24192  fclsfnflim  24235  flimfnfcls  24236  alexsubALTlem3  24257  alexsubALTlem4  24258  tsmsgsum  24347  tsmsres  24352  tsmsxplem1  24361  ustund  24430  trust  24437  ustuqtop1  24449  prdsdsf  24575  prdsxmetlem  24576  prdsmet  24578  prdsbl  24699  prdsxmslem2  24737  restmetu  24778  icccmplem2  25032  rrxmval  25615  rrxmet  25618  rrxdstprj1  25619  ovolunlem1  25707  ovolunnul  25710  nulmbl2  25746  volun  25755  volcn  25816  itgsplitioo  26048  limcvallem  26081  limcdif  26086  ellimc2  26087  limcres  26096  limccnp  26101  limccnp2  26102  limcco  26103  dvreslem  26119  dvres2lem  26120  dvaddbr  26148  dvmulbr  26149  lhop2  26225  dvcnvrelem2  26228  elply2  26404  plyf  26406  elplyr  26409  elplyd  26410  ply1term  26412  ply0  26416  plyeq0lem  26418  plyeq0  26419  plyaddlem  26423  plymullem  26424  dgrlem  26437  coeidlem  26445  plyco  26449  plycj  26485  plycjOLD  26487  aannenlem2  26543  xrlimcnp  27184  perfectlem2  27445  noextend  27881  sltsun1  28032  sltsun2  28033  cutlt  28176  lrrecpred  28188  addsproplem2  28214  addsuniflem  28245  addbday  28262  negsid  28285  mulsproplem9  28368  sltmuls1  28391  sltmuls2  28392  precsexlem8  28458  precsexlem11  28461  onaddscl  28521  bdaypw2n0bndlem  28707  shlej1  31783  shlub  31837  disjiunel  33012  fcoinver  33020  gsumzresunsn  33446  gsumwun  33460  elrgspnsubrunlem1  33631  elrgspnsubrunlem2  33632  elrgspnsubrun  33633  elrspunsn  33801  mxidlprm  33817  qsdrngilem  33840  esplyind  34029  lindsun  34079  fldgenfldext  34122  evls1fldgencl  34124  fldextrspunlem1  34129  fldextrspunfld  34130  fldextrspunlem2  34131  fldextrspundgdvdslem  34134  fldextrspundgdvds  34135  algextdeglem1  34171  algextdeglem2  34172  algextdeglem3  34173  algextdeglem4  34174  algextdeglem5  34175  rtelextdg2  34181  constrextdg2lem  34202  constrext2chnlem  34204  constrfiss  34205  constrllcllem  34206  constrlccllem  34207  constrcccllem  34208  ordtrestNEW  34375  carsggect  34773  eulerpartlemt  34826  hgt750lemb  35108  hgt750leme  35110  bnj1136  35450  bnj1452  35505  erdszelem8  35727  mclsssvlem  36091  mclsax  36098  mclsind  36099  mthmpps  36111  mclsppslem  36112  topjoin  36933  weiunse  37036  poimirlem32  38360  ftc1anclem7  38407  ftc1anc  38409  prdsbnd  38502  rrnequiv  38544  pclfinN  40732  dochdmj1  42222  djhspss  42238  djhunssN  42241  djhlsmcl  42246  dvh4dimlem  42275  dvhdimlem  42276  lclkrlem2c  42341  lclkrlem2v  42360  mapdh9a  42621  hdmapval0  42665  hdmapval3lemN  42669  hdmap10lem  42671  deg1gprod  42965  dvun  43178  elrfi  43483  cmpfiiin  43486  istopclsd  43489  mzpcompact2lem  43540  eldioph2lem2  43550  eldioph2  43551  rngunsnply  43954  idomsubgmo  43978  omabs2  44117  dfrcl2  44458  iunrelexp0  44486  relexp0a  44500  brtrclfv2  44511  frege77d  44530  frege109d  44541  frege131d  44548  clsk3nimkb  44824  isotone1  44832  ntrclskb  44853  ntrclsk3  44854  ntrclsk13  44855  ntrneixb  44879  ntrneix3  44881  ntrneix13  44883  infxrpnf  46218  pimxrneun  46260  mccllem  46371  limciccioolb  46395  limcicciooub  46409  limcresiooub  46414  limcresioolb  46415  icccncfext  46659  dvnprodlem2  46719  ovolsplit  46760  fourierdlem20  46899  fourierdlem46  46924  fourierdlem48  46926  fourierdlem49  46927  fourierdlem50  46928  fourierdlem51  46929  fourierdlem54  46932  fourierdlem64  46942  fourierdlem76  46954  fourierdlem101  46979  fourierdlem102  46980  fourierdlem103  46981  fourierdlem104  46982  fourierdlem114  46992  sge0resplit  47178  sge0xaddlem1  47205  ismeannd  47239  caragenuncl  47285  omeunle  47288  isomenndlem  47302  hoidmvlelem2  47368  hoidmvlelem3  47369  hoidmvlelem4  47370  perfectALTVlem2  48545  gpgprismgriedgdmss  48875  pgindlem  50550