Theorem unssd 4132

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3887   ⊆ wss 3889

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 2708

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

This theorem is referenced by:  uneqdifeq  4432  tpssi  4781  sofld  6151  unima  6915  fr3nr  7726  ordsuci  7762  resf1extb  7885  resf1ext2b  7886  xpord2pred  8095  xpord3pred  8102  frrlem13  8248  naddcllem  8612  ralxpmap  8844  marypha1lem  9346  wemapso2lem  9467  unwf  9734  rankunb  9774  ackbij1lem6  10146  ackbij1lem16  10156  ssfin4  10232  isfin1-3  10308  ttukeylem7  10437  fpwwe2lem12  10565  wuncval2  10670  inar1  10698  un0addcl  12470  un0mulcl  12471  ssfzunsnext  13523  fzosplit  13647  fzouzsplit  13649  hashf1lem1  14417  ccatrn  14552  trclfvlb3  14973  trclun  14976  relexpfld  15011  saddisj  16434  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  lcmfunsnlem2  16609  lcmfun  16614  prmreclem5  16891  4sqlem11  16926  4sqlem19  16934  vdwlem1  16952  vdwlem12  16963  ramub1lem1  16997  ramub1lem2  16998  mrieqvlemd  17595  mreexmrid  17609  mreexexlem2d  17611  mreexexlem3d  17612  mreexexlem4d  17613  acsfiindd  18519  tsrdir  18570  f1omvdco2  19423  symgsssg  19442  symggen  19445  lsmunss  19634  efgsfo  19714  lsptpcl  20974  lspun  20982  lsmsp  21081  lspsolvlem  21140  lspsolv  21141  lsppratlem3  21147  lsppratlem4  21148  islbs3  21153  lbsextlem4  21159  aspval2  21878  evlseu  22061  mhpaddcl  22117  clslp  23113  neitr  23145  ordtuni  23155  ordtbas2  23156  ordtbas  23157  ordtrest  23167  cmpcld  23367  comppfsc  23497  1stckgenlem  23518  1stckgen  23519  ptbasfi  23546  fbun  23805  trfil2  23852  isufil2  23873  ufileu  23884  filufint  23885  fmfnfm  23923  hausflim  23946  flimclslem  23949  fclsfnflim  23992  flimfnfcls  23993  alexsubALTlem3  24014  alexsubALTlem4  24015  tsmsgsum  24104  tsmsres  24109  tsmsxplem1  24118  ustund  24187  trust  24194  ustuqtop1  24206  prdsdsf  24332  prdsxmetlem  24333  prdsmet  24335  prdsbl  24456  prdsxmslem2  24494  restmetu  24535  icccmplem2  24789  rrxmval  25372  rrxmet  25375  rrxdstprj1  25376  ovolunlem1  25464  ovolunnul  25467  nulmbl2  25503  volun  25512  volcn  25573  itgsplitioo  25805  limcvallem  25838  limcdif  25843  ellimc2  25844  limcres  25853  limccnp  25858  limccnp2  25859  limcco  25860  dvreslem  25876  dvres2lem  25877  dvaddbr  25905  dvmulbr  25906  lhop2  25982  dvcnvrelem2  25985  elply2  26161  plyf  26163  elplyr  26166  elplyd  26167  ply1term  26169  ply0  26173  plyeq0lem  26175  plyeq0  26176  plyaddlem  26180  plymullem  26181  dgrlem  26194  coeidlem  26202  plyco  26206  plycj  26242  plycjOLD  26244  aannenlem2  26295  xrlimcnp  26932  perfectlem2  27193  noextend  27630  sltsun1  27780  sltsun2  27781  cutlt  27924  lrrecpred  27936  addsproplem2  27962  addsuniflem  27993  addbday  28010  negsid  28033  mulsproplem9  28116  sltmuls1  28139  sltmuls2  28140  precsexlem8  28206  precsexlem11  28209  onaddscl  28269  bdaypw2n0bndlem  28455  shlej1  31431  shlub  31485  disjiunel  32666  fcoinver  32674  gsumzresunsn  33123  gsumwun  33137  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  elrgspnsubrun  33310  lsmidl  33461  elrspunsn  33489  mxidlprm  33530  qsdrngilem  33554  esplyind  33719  lindsun  33769  fldgenfldext  33812  evls1fldgencl  33814  fldextrspunlem1  33819  fldextrspunfld  33820  fldextrspunlem2  33821  fldextrspundgdvdslem  33824  fldextrspundgdvds  33825  algextdeglem1  33861  algextdeglem2  33862  algextdeglem3  33863  algextdeglem4  33864  algextdeglem5  33865  rtelextdg2  33871  constrextdg2lem  33892  constrext2chnlem  33894  constrfiss  33895  constrllcllem  33896  constrlccllem  33897  constrcccllem  33898  ordtrestNEW  34065  carsggect  34462  eulerpartlemt  34515  hgt750lemb  34800  hgt750leme  34802  bnj1136  35139  bnj1452  35194  erdszelem8  35380  mclsssvlem  35744  mclsax  35751  mclsind  35752  mthmpps  35764  mclsppslem  35765  topjoin  36547  weiunse  36650  poimirlem32  37973  ftc1anclem7  38020  ftc1anc  38022  prdsbnd  38114  rrnequiv  38156  pclfinN  40346  dochdmj1  41836  djhspss  41852  djhunssN  41855  djhlsmcl  41860  dvh4dimlem  41889  dvhdimlem  41890  lclkrlem2c  41955  lclkrlem2v  41974  mapdh9a  42235  hdmapval0  42279  hdmapval3lemN  42283  hdmap10lem  42285  deg1gprod  42579  dvun  42791  elrfi  43126  cmpfiiin  43129  istopclsd  43132  mzpcompact2lem  43183  eldioph2lem2  43193  eldioph2  43194  rngunsnply  43597  idomsubgmo  43621  omabs2  43760  dfrcl2  44101  iunrelexp0  44129  relexp0a  44143  brtrclfv2  44154  frege77d  44173  frege109d  44184  frege131d  44191  clsk3nimkb  44467  isotone1  44475  ntrclskb  44496  ntrclsk3  44497  ntrclsk13  44498  ntrneixb  44522  ntrneix3  44524  ntrneix13  44526  infxrpnf  45874  pimxrneun  45916  mccllem  46027  limciccioolb  46051  limcicciooub  46065  limcresiooub  46070  limcresioolb  46071  icccncfext  46315  dvnprodlem2  46375  ovolsplit  46416  fourierdlem20  46555  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem51  46585  fourierdlem54  46588  fourierdlem64  46598  fourierdlem76  46610  fourierdlem101  46635  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem114  46648  sge0resplit  46834  sge0xaddlem1  46861  ismeannd  46895  caragenuncl  46941  omeunle  46944  isomenndlem  46958  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  perfectALTVlem2  48198  gpgprismgriedgdmss  48528  pgindlem  50190