Theorem unssd 4144

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918

This theorem is referenced by:  uneqdifeq  4445  tpssi  4794  sofld  6145  unima  6909  fr3nr  7717  ordsuci  7753  resf1extb  7876  resf1ext2b  7877  xpord2pred  8087  xpord3pred  8094  frrlem13  8240  naddcllem  8604  ralxpmap  8834  marypha1lem  9336  wemapso2lem  9457  unwf  9722  rankunb  9762  ackbij1lem6  10134  ackbij1lem16  10144  ssfin4  10220  isfin1-3  10296  ttukeylem7  10425  fpwwe2lem12  10553  wuncval2  10658  inar1  10686  un0addcl  12434  un0mulcl  12435  ssfzunsnext  13485  fzosplit  13608  fzouzsplit  13610  hashf1lem1  14378  ccatrn  14513  trclfvlb3  14934  trclun  14937  relexpfld  14972  saddisj  16392  lcmfunsnlem2lem1  16565  lcmfunsnlem2lem2  16566  lcmfunsnlem2  16567  lcmfun  16572  prmreclem5  16848  4sqlem11  16883  4sqlem19  16891  vdwlem1  16909  vdwlem12  16920  ramub1lem1  16954  ramub1lem2  16955  mrieqvlemd  17552  mreexmrid  17566  mreexexlem2d  17568  mreexexlem3d  17569  mreexexlem4d  17570  acsfiindd  18476  tsrdir  18527  f1omvdco2  19377  symgsssg  19396  symggen  19399  lsmunss  19588  efgsfo  19668  lsptpcl  20930  lspun  20938  lsmsp  21038  lspsolvlem  21097  lspsolv  21098  lsppratlem3  21104  lsppratlem4  21105  islbs3  21110  lbsextlem4  21116  aspval2  21854  evlseu  22038  mhpaddcl  22094  clslp  23092  neitr  23124  ordtuni  23134  ordtbas2  23135  ordtbas  23136  ordtrest  23146  cmpcld  23346  comppfsc  23476  1stckgenlem  23497  1stckgen  23498  ptbasfi  23525  fbun  23784  trfil2  23831  isufil2  23852  ufileu  23863  filufint  23864  fmfnfm  23902  hausflim  23925  flimclslem  23928  fclsfnflim  23971  flimfnfcls  23972  alexsubALTlem3  23993  alexsubALTlem4  23994  tsmsgsum  24083  tsmsres  24088  tsmsxplem1  24097  ustund  24166  trust  24173  ustuqtop1  24185  prdsdsf  24311  prdsxmetlem  24312  prdsmet  24314  prdsbl  24435  prdsxmslem2  24473  restmetu  24514  icccmplem2  24768  rrxmval  25361  rrxmet  25364  rrxdstprj1  25365  ovolunlem1  25454  ovolunnul  25457  nulmbl2  25493  volun  25502  volcn  25563  itgsplitioo  25795  limcvallem  25828  limcdif  25833  ellimc2  25834  limcres  25843  limccnp  25848  limccnp2  25849  limcco  25850  dvreslem  25866  dvres2lem  25867  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  lhop2  25976  dvcnvrelem2  25979  elply2  26157  plyf  26159  elplyr  26162  elplyd  26163  ply1term  26165  ply0  26169  plyeq0lem  26171  plyeq0  26172  plyaddlem  26176  plymullem  26177  dgrlem  26190  coeidlem  26198  plyco  26202  plycj  26239  plycjOLD  26241  aannenlem2  26293  xrlimcnp  26934  perfectlem2  27197  noextend  27634  sltsun1  27784  sltsun2  27785  cutlt  27928  lrrecpred  27940  addsproplem2  27966  addsuniflem  27997  addbday  28014  negsid  28037  mulsproplem9  28120  sltmuls1  28143  sltmuls2  28144  precsexlem8  28210  precsexlem11  28213  onaddscl  28273  bdaypw2n0bndlem  28459  shlej1  31435  shlub  31489  disjiunel  32671  fcoinver  32679  gsumzresunsn  33145  gsumwun  33158  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  elrgspnsubrun  33331  lsmidl  33482  elrspunsn  33510  mxidlprm  33551  qsdrngilem  33575  esplyind  33731  lindsun  33782  fldgenfldext  33825  evls1fldgencl  33827  fldextrspunlem1  33832  fldextrspunfld  33833  fldextrspunlem2  33834  fldextrspundgdvdslem  33837  fldextrspundgdvds  33838  algextdeglem1  33874  algextdeglem2  33875  algextdeglem3  33876  algextdeglem4  33877  algextdeglem5  33878  rtelextdg2  33884  constrextdg2lem  33905  constrext2chnlem  33907  constrfiss  33908  constrllcllem  33909  constrlccllem  33910  constrcccllem  33911  ordtrestNEW  34078  carsggect  34475  eulerpartlemt  34528  hgt750lemb  34813  hgt750leme  34815  bnj1136  35153  bnj1452  35208  erdszelem8  35392  mclsssvlem  35756  mclsax  35763  mclsind  35764  mthmpps  35776  mclsppslem  35777  topjoin  36559  weiunse  36662  poimirlem32  37853  ftc1anclem7  37900  ftc1anc  37902  prdsbnd  37994  rrnequiv  38036  pclfinN  40160  dochdmj1  41650  djhspss  41666  djhunssN  41669  djhlsmcl  41674  dvh4dimlem  41703  dvhdimlem  41704  lclkrlem2c  41769  lclkrlem2v  41788  mapdh9a  42049  hdmapval0  42093  hdmapval3lemN  42097  hdmap10lem  42099  deg1gprod  42394  dvun  42614  elrfi  42936  cmpfiiin  42939  istopclsd  42942  mzpcompact2lem  42993  eldioph2lem2  43003  eldioph2  43004  rngunsnply  43411  idomsubgmo  43435  omabs2  43574  dfrcl2  43915  iunrelexp0  43943  relexp0a  43957  brtrclfv2  43968  frege77d  43987  frege109d  43998  frege131d  44005  clsk3nimkb  44281  isotone1  44289  ntrclskb  44310  ntrclsk3  44311  ntrclsk13  44312  ntrneixb  44336  ntrneix3  44338  ntrneix13  44340  infxrpnf  45690  pimxrneun  45732  mccllem  45843  limciccioolb  45867  limcicciooub  45881  limcresiooub  45886  limcresioolb  45887  icccncfext  46131  dvnprodlem2  46191  ovolsplit  46232  fourierdlem20  46371  fourierdlem46  46396  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem51  46401  fourierdlem54  46404  fourierdlem64  46414  fourierdlem76  46426  fourierdlem101  46451  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem114  46464  sge0resplit  46650  sge0xaddlem1  46677  ismeannd  46711  caragenuncl  46757  omeunle  46760  isomenndlem  46774  hoidmvlelem2  46840  hoidmvlelem3  46841  hoidmvlelem4  46842  perfectALTVlem2  47968  gpgprismgriedgdmss  48298  pgindlem  49960