Theorem unssd 4139

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3895   ⊆ wss 3897

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914

This theorem is referenced by:  uneqdifeq  4440  tpssi  4787  sofld  6134  unima  6897  fr3nr  7705  ordsuci  7741  resf1extb  7864  resf1ext2b  7865  xpord2pred  8075  xpord3pred  8082  frrlem13  8228  naddcllem  8591  ralxpmap  8820  marypha1lem  9317  wemapso2lem  9438  unwf  9703  rankunb  9743  ackbij1lem6  10115  ackbij1lem16  10125  ssfin4  10201  isfin1-3  10277  ttukeylem7  10406  fpwwe2lem12  10533  wuncval2  10638  inar1  10666  un0addcl  12414  un0mulcl  12415  ssfzunsnext  13469  fzosplit  13592  fzouzsplit  13594  hashf1lem1  14362  ccatrn  14497  trclfvlb3  14918  trclun  14921  relexpfld  14956  saddisj  16376  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  lcmfun  16556  prmreclem5  16832  4sqlem11  16867  4sqlem19  16875  vdwlem1  16893  vdwlem12  16904  ramub1lem1  16938  ramub1lem2  16939  mrieqvlemd  17535  mreexmrid  17549  mreexexlem2d  17551  mreexexlem3d  17552  mreexexlem4d  17553  acsfiindd  18459  tsrdir  18510  f1omvdco2  19360  symgsssg  19379  symggen  19382  lsmunss  19571  efgsfo  19651  lsptpcl  20912  lspun  20920  lsmsp  21020  lspsolvlem  21079  lspsolv  21080  lsppratlem3  21086  lsppratlem4  21087  islbs3  21092  lbsextlem4  21098  aspval2  21835  evlseu  22018  mhpaddcl  22066  clslp  23063  neitr  23095  ordtuni  23105  ordtbas2  23106  ordtbas  23107  ordtrest  23117  cmpcld  23317  comppfsc  23447  1stckgenlem  23468  1stckgen  23469  ptbasfi  23496  fbun  23755  trfil2  23802  isufil2  23823  ufileu  23834  filufint  23835  fmfnfm  23873  hausflim  23896  flimclslem  23899  fclsfnflim  23942  flimfnfcls  23943  alexsubALTlem3  23964  alexsubALTlem4  23965  tsmsgsum  24054  tsmsres  24059  tsmsxplem1  24068  ustund  24137  trust  24144  ustuqtop1  24156  prdsdsf  24282  prdsxmetlem  24283  prdsmet  24285  prdsbl  24406  prdsxmslem2  24444  restmetu  24485  icccmplem2  24739  rrxmval  25332  rrxmet  25335  rrxdstprj1  25336  ovolunlem1  25425  ovolunnul  25428  nulmbl2  25464  volun  25473  volcn  25534  itgsplitioo  25766  limcvallem  25799  limcdif  25804  ellimc2  25805  limcres  25814  limccnp  25819  limccnp2  25820  limcco  25821  dvreslem  25837  dvres2lem  25838  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  lhop2  25947  dvcnvrelem2  25950  elply2  26128  plyf  26130  elplyr  26133  elplyd  26134  ply1term  26136  ply0  26140  plyeq0lem  26142  plyeq0  26143  plyaddlem  26147  plymullem  26148  dgrlem  26161  coeidlem  26169  plyco  26173  plycj  26210  plycjOLD  26212  aannenlem2  26264  xrlimcnp  26905  perfectlem2  27168  noextend  27605  ssltun1  27749  ssltun2  27750  cutlt  27876  lrrecpred  27887  addsproplem2  27913  addsuniflem  27944  addsbday  27960  negsid  27983  mulsproplem9  28063  ssltmul1  28086  ssltmul2  28087  precsexlem8  28152  precsexlem11  28155  onaddscl  28210  shlej1  31340  shlub  31394  disjiunel  32576  fcoinver  32584  gsumzresunsn  33036  gsumwun  33045  elrgspnsubrunlem1  33214  elrgspnsubrunlem2  33215  elrgspnsubrun  33216  lsmidl  33366  elrspunsn  33394  mxidlprm  33435  qsdrngilem  33459  lindsun  33638  fldgenfldext  33681  evls1fldgencl  33683  fldextrspunlem1  33688  fldextrspunfld  33689  fldextrspunlem2  33690  fldextrspundgdvdslem  33693  fldextrspundgdvds  33694  algextdeglem1  33730  algextdeglem2  33731  algextdeglem3  33732  algextdeglem4  33733  algextdeglem5  33734  rtelextdg2  33740  constrextdg2lem  33761  constrext2chnlem  33763  constrfiss  33764  constrllcllem  33765  constrlccllem  33766  constrcccllem  33767  ordtrestNEW  33934  carsggect  34331  eulerpartlemt  34384  hgt750lemb  34669  hgt750leme  34671  bnj1136  35009  bnj1452  35064  erdszelem8  35242  mclsssvlem  35606  mclsax  35613  mclsind  35614  mthmpps  35626  mclsppslem  35627  topjoin  36409  weiunse  36512  poimirlem32  37702  ftc1anclem7  37749  ftc1anc  37751  prdsbnd  37843  rrnequiv  37885  pclfinN  40009  dochdmj1  41499  djhspss  41515  djhunssN  41518  djhlsmcl  41523  dvh4dimlem  41552  dvhdimlem  41553  lclkrlem2c  41618  lclkrlem2v  41637  mapdh9a  41898  hdmapval0  41942  hdmapval3lemN  41946  hdmap10lem  41948  deg1gprod  42243  dvun  42462  elrfi  42797  cmpfiiin  42800  istopclsd  42803  mzpcompact2lem  42854  eldioph2lem2  42864  eldioph2  42865  rngunsnply  43272  idomsubgmo  43296  omabs2  43435  dfrcl2  43777  iunrelexp0  43805  relexp0a  43819  brtrclfv2  43830  frege77d  43849  frege109d  43860  frege131d  43867  clsk3nimkb  44143  isotone1  44151  ntrclskb  44172  ntrclsk3  44173  ntrclsk13  44174  ntrneixb  44198  ntrneix3  44200  ntrneix13  44202  infxrpnf  45554  pimxrneun  45596  mccllem  45707  limciccioolb  45731  limcicciooub  45745  limcresiooub  45750  limcresioolb  45751  icccncfext  45995  dvnprodlem2  46055  ovolsplit  46096  fourierdlem20  46235  fourierdlem46  46260  fourierdlem48  46262  fourierdlem49  46263  fourierdlem50  46264  fourierdlem51  46265  fourierdlem54  46268  fourierdlem64  46278  fourierdlem76  46290  fourierdlem101  46315  fourierdlem102  46316  fourierdlem103  46317  fourierdlem104  46318  fourierdlem114  46328  sge0resplit  46514  sge0xaddlem1  46541  ismeannd  46575  caragenuncl  46621  omeunle  46624  isomenndlem  46638  hoidmvlelem2  46704  hoidmvlelem3  46705  hoidmvlelem4  46706  perfectALTVlem2  47832  gpgprismgriedgdmss  48162  pgindlem  49826