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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921

This theorem is used by:  uneqdifeq  4452  tpssi  4802  sofld  6184  unima  6956  fr3nr  7769  ordsuci  7805  resf1extb  7929  resf1ext2b  7930  xpord2pred  8139  xpord3pred  8146  frrlem13  8293  naddcllem  8660  ralxpmap  8892  marypha1lem  9391  wemapso2lem  9512  unwf  9780  rankunb  9820  ackbij1lem6  10214  ackbij1lem16  10224  ssfin4  10300  isfin1-3  10376  ttukeylem7  10505  fpwwe2lem12  10633  wuncval2  10738  inar1  10766  un0addcl  12543  un0mulcl  12544  ssfzunsnext  13604  fzosplit  13728  fzouzsplit  13730  hashf1lem1  14499  ccatrn  14634  trclfvlb3  15055  trclun  15058  relexpfld  15093  saddisj  16529  lcmfunsnlem2lem1  16702  lcmfunsnlem2lem2  16703  lcmfunsnlem2  16704  lcmfun  16709  prmreclem5  16986  4sqlem11  17021  4sqlem19  17029  vdwlem1  17047  vdwlem12  17058  ramub1lem1  17092  ramub1lem2  17093  mrieqvlemd  17691  mreexmrid  17705  mreexexlem2d  17707  mreexexlem3d  17708  mreexexlem4d  17709  acsfiindd  18615  tsrdir  18666  f1omvdco2  19524  symgsssg  19543  symggen  19546  lsmunss  19735  efgsfo  19815  lsptpcl  21111  lspun  21119  lsmsp  21218  lspsolvlem  21277  lspsolv  21278  lsppratlem3  21284  lsppratlem4  21285  islbs3  21290  lbsextlem4  21296  lsmidl  21395  aspval2  22059  evlseu  22245  mhpaddcl  22325  clslp  23316  neitr  23348  ordtuni  23358  ordtbas2  23359  ordtbas  23360  ordtrest  23370  cmpcld  23570  comppfsc  23700  1stckgenlem  23721  1stckgen  23722  ptbasfi  23749  fbun  24008  trfil2  24055  isufil2  24076  ufileu  24087  filufint  24088  fmfnfm  24126  hausflim  24149  flimclslem  24152  fclsfnflim  24195  flimfnfcls  24196  alexsubALTlem3  24217  alexsubALTlem4  24218  tsmsgsum  24307  tsmsres  24312  tsmsxplem1  24321  ustund  24390  trust  24397  ustuqtop1  24409  prdsdsf  24535  prdsxmetlem  24536  prdsmet  24538  prdsbl  24659  prdsxmslem2  24697  restmetu  24738  icccmplem2  24992  rrxmval  25575  rrxmet  25578  rrxdstprj1  25579  ovolunlem1  25667  ovolunnul  25670  nulmbl2  25706  volun  25715  volcn  25776  itgsplitioo  26008  limcvallem  26041  limcdif  26046  ellimc2  26047  limcres  26056  limccnp  26061  limccnp2  26062  limcco  26063  dvreslem  26079  dvres2lem  26080  dvaddbr  26108  dvmulbr  26109  lhop2  26185  dvcnvrelem2  26188  elply2  26364  plyf  26366  elplyr  26369  elplyd  26370  ply1term  26372  ply0  26376  plyeq0lem  26378  plyeq0  26379  plyaddlem  26383  plymullem  26384  dgrlem  26397  coeidlem  26405  plyco  26409  plycj  26445  plycjOLD  26447  aannenlem2  26503  xrlimcnp  27144  perfectlem2  27405  noextend  27841  sltsun1  27992  sltsun2  27993  cutlt  28136  lrrecpred  28148  addsproplem2  28174  addsuniflem  28205  addbday  28222  negsid  28245  mulsproplem9  28328  sltmuls1  28351  sltmuls2  28352  precsexlem8  28418  precsexlem11  28421  onaddscl  28481  bdaypw2n0bndlem  28667  shlej1  31723  shlub  31777  disjiunel  32952  fcoinver  32960  gsumzresunsn  33391  gsumwun  33405  elrgspnsubrunlem1  33576  elrgspnsubrunlem2  33577  elrgspnsubrun  33578  elrspunsn  33746  mxidlprm  33762  qsdrngilem  33785  esplyind  33974  lindsun  34024  fldgenfldext  34067  evls1fldgencl  34069  fldextrspunlem1  34074  fldextrspunfld  34075  fldextrspunlem2  34076  fldextrspundgdvdslem  34079  fldextrspundgdvds  34080  algextdeglem1  34116  algextdeglem2  34117  algextdeglem3  34118  algextdeglem4  34119  algextdeglem5  34120  rtelextdg2  34126  constrextdg2lem  34147  constrext2chnlem  34149  constrfiss  34150  constrllcllem  34151  constrlccllem  34152  constrcccllem  34153  ordtrestNEW  34320  carsggect  34717  eulerpartlemt  34770  hgt750lemb  35052  hgt750leme  35054  bnj1136  35394  bnj1452  35449  erdszelem8  35698  mclsssvlem  36062  mclsax  36069  mclsind  36070  mthmpps  36082  mclsppslem  36083  topjoin  36904  weiunse  37007  poimirlem32  38331  ftc1anclem7  38378  ftc1anc  38380  prdsbnd  38472  rrnequiv  38514  pclfinN  40702  dochdmj1  42192  djhspss  42208  djhunssN  42211  djhlsmcl  42216  dvh4dimlem  42245  dvhdimlem  42246  lclkrlem2c  42311  lclkrlem2v  42330  mapdh9a  42591  hdmapval0  42635  hdmapval3lemN  42639  hdmap10lem  42641  deg1gprod  42935  dvun  43148  elrfi  43453  cmpfiiin  43456  istopclsd  43459  mzpcompact2lem  43510  eldioph2lem2  43520  eldioph2  43521  rngunsnply  43924  idomsubgmo  43948  omabs2  44087  dfrcl2  44428  iunrelexp0  44456  relexp0a  44470  brtrclfv2  44481  frege77d  44500  frege109d  44511  frege131d  44518  clsk3nimkb  44794  isotone1  44802  ntrclskb  44823  ntrclsk3  44824  ntrclsk13  44825  ntrneixb  44849  ntrneix3  44851  ntrneix13  44853  infxrpnf  46188  pimxrneun  46230  mccllem  46341  limciccioolb  46365  limcicciooub  46379  limcresiooub  46384  limcresioolb  46385  icccncfext  46629  dvnprodlem2  46689  ovolsplit  46730  fourierdlem20  46869  fourierdlem46  46894  fourierdlem48  46896  fourierdlem49  46897  fourierdlem50  46898  fourierdlem51  46899  fourierdlem54  46902  fourierdlem64  46912  fourierdlem76  46924  fourierdlem101  46949  fourierdlem102  46950  fourierdlem103  46951  fourierdlem104  46952  fourierdlem114  46962  sge0resplit  47148  sge0xaddlem1  47175  ismeannd  47209  caragenuncl  47255  omeunle  47258  isomenndlem  47272  hoidmvlelem2  47338  hoidmvlelem3  47339  hoidmvlelem4  47340  perfectALTVlem2  48515  gpgprismgriedgdmss  48845  pgindlem  50521