Theorem unssd 4187

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

Syntax hints:   → wi 4   ∧ wa 397   ∪ cun 3947   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966

This theorem is referenced by:  uneqdifeq  4493  tpssi  4840  sofld  6187  unima  6967  fr3nr  7759  ordsuci  7796  sucexeloniOLD  7798  suceloniOLD  7800  xpord2pred  8131  xpord3pred  8138  frrlem13  8283  naddcllem  8675  ralxpmap  8890  marypha1lem  9428  wemapso2lem  9547  unwf  9805  rankunb  9845  ackbij1lem6  10220  ackbij1lem16  10230  ssfin4  10305  isfin1-3  10381  ttukeylem7  10510  fpwwe2lem12  10637  wuncval2  10742  inar1  10770  un0addcl  12505  un0mulcl  12506  ssfzunsnext  13546  fzosplit  13665  fzouzsplit  13667  hashf1lem1  14415  hashf1lem1OLD  14416  ccatrn  14539  trclfvlb3  14958  trclun  14961  relexpfld  14996  saddisj  16406  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  lcmfunsnlem2  16577  lcmfun  16582  prmreclem5  16853  4sqlem11  16888  4sqlem19  16896  vdwlem1  16914  vdwlem12  16925  ramub1lem1  16959  ramub1lem2  16960  mrieqvlemd  17573  mreexmrid  17587  mreexexlem2d  17589  mreexexlem3d  17590  mreexexlem4d  17591  acsfiindd  18506  tsrdir  18557  f1omvdco2  19316  symgsssg  19335  symggen  19338  lsmunss  19527  efgsfo  19607  lsptpcl  20590  lspun  20598  lsmsp  20697  lspsolvlem  20755  lspsolv  20756  lsppratlem3  20762  lsppratlem4  20763  islbs3  20768  lbsextlem4  20774  aspval2  21452  evlseu  21646  mhpaddcl  21694  clslp  22652  neitr  22684  ordtuni  22694  ordtbas2  22695  ordtbas  22696  ordtrest  22706  cmpcld  22906  comppfsc  23036  1stckgenlem  23057  1stckgen  23058  ptbasfi  23085  fbun  23344  trfil2  23391  isufil2  23412  ufileu  23423  filufint  23424  fmfnfm  23462  hausflim  23485  flimclslem  23488  fclsfnflim  23531  flimfnfcls  23532  alexsubALTlem3  23553  alexsubALTlem4  23554  tsmsgsum  23643  tsmsres  23648  tsmsxplem1  23657  ustund  23726  trust  23734  ustuqtop1  23746  prdsdsf  23873  prdsxmetlem  23874  prdsmet  23876  prdsbl  24000  prdsxmslem2  24038  restmetu  24079  icccmplem2  24339  rrxmval  24922  rrxmet  24925  rrxdstprj1  24926  ovolunlem1  25014  ovolunnul  25017  nulmbl2  25053  volun  25062  volcn  25123  itgsplitioo  25355  limcvallem  25388  limcdif  25393  ellimc2  25394  limcres  25403  limccnp  25408  limccnp2  25409  limcco  25410  dvreslem  25426  dvres2lem  25427  dvaddbr  25455  dvmulbr  25456  lhop2  25532  dvcnvrelem2  25535  elply2  25710  plyf  25712  elplyr  25715  elplyd  25716  ply1term  25718  ply0  25722  plyeq0lem  25724  plyeq0  25725  plyaddlem  25729  plymullem  25730  dgrlem  25743  coeidlem  25751  plyco  25755  plycj  25791  aannenlem2  25842  xrlimcnp  26473  perfectlem2  26733  noextend  27169  ssltun1  27309  ssltun2  27310  cutlt  27419  lrrecpred  27428  addsproplem2  27454  addsuniflem  27484  negsid  27515  mulsproplem9  27580  ssltmul1  27602  ssltmul2  27603  precsexlem8  27660  precsexlem11  27663  shlej1  30613  shlub  30667  disjiunel  31827  fcoinver  31835  gsumzresunsn  32206  lsmidl  32511  elrspunsn  32547  mxidlprm  32586  qsdrngilem  32608  lindsun  32710  algextdeglem1  32772  ordtrestNEW  32901  carsggect  33317  eulerpartlemt  33370  hgt750lemb  33668  hgt750leme  33670  bnj1136  34008  bnj1452  34063  erdszelem8  34189  mclsssvlem  34553  mclsax  34560  mclsind  34561  mthmpps  34573  mclsppslem  34574  gg-dvmulbr  35175  topjoin  35250  poimirlem32  36520  ftc1anclem7  36567  ftc1anc  36569  prdsbnd  36661  rrnequiv  36703  pclfinN  38771  dochdmj1  40261  djhspss  40277  djhunssN  40280  djhlsmcl  40285  dvh4dimlem  40314  dvhdimlem  40315  lclkrlem2c  40380  lclkrlem2v  40399  mapdh9a  40660  hdmapval0  40704  hdmapval3lemN  40708  hdmap10lem  40710  elrfi  41432  cmpfiiin  41435  istopclsd  41438  mzpcompact2lem  41489  eldioph2lem2  41499  eldioph2  41500  rngunsnply  41915  idomsubgmo  41940  omabs2  42082  dfrcl2  42425  iunrelexp0  42453  relexp0a  42467  brtrclfv2  42478  frege77d  42497  frege109d  42508  frege131d  42515  clsk3nimkb  42791  isotone1  42799  ntrclskb  42820  ntrclsk3  42821  ntrclsk13  42822  ntrneixb  42846  ntrneix3  42848  ntrneix13  42850  infxrpnf  44156  pimxrneun  44199  mccllem  44313  limciccioolb  44337  limcicciooub  44353  limcresiooub  44358  limcresioolb  44359  icccncfext  44603  dvnprodlem2  44663  ovolsplit  44704  fourierdlem20  44843  fourierdlem46  44868  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem51  44873  fourierdlem54  44876  fourierdlem64  44886  fourierdlem76  44898  fourierdlem101  44923  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem114  44936  sge0resplit  45122  sge0xaddlem1  45149  ismeannd  45183  caragenuncl  45229  omeunle  45232  isomenndlem  45246  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem4  45314  perfectALTVlem2  46390  pgindlem  47760