Theorem unssd 4124

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-un 3896  df-in 3898  df-ss 3908

This theorem is referenced by:  uneqdifeq  4428  tpssi  4774  sofld  6087  unima  6837  fr3nr  7613  suceloni  7648  frrlem13  8098  ralxpmap  8658  marypha1lem  9153  wemapso2lem  9272  dftrpred3g  9464  unwf  9552  rankunb  9592  ackbij1lem6  9965  ackbij1lem16  9975  ssfin4  10050  isfin1-3  10126  ttukeylem7  10255  fpwwe2lem12  10382  wuncval2  10487  inar1  10515  un0addcl  12249  un0mulcl  12250  ssfzunsnext  13283  fzosplit  13401  fzouzsplit  13403  hashf1lem1  14149  hashf1lem1OLD  14150  ccatrn  14275  trclfvlb3  14703  trclun  14706  relexpfld  14741  saddisj  16153  lcmfunsnlem2lem1  16324  lcmfunsnlem2lem2  16325  lcmfunsnlem2  16326  lcmfun  16331  prmreclem5  16602  4sqlem11  16637  4sqlem19  16645  vdwlem1  16663  vdwlem12  16674  ramub1lem1  16708  ramub1lem2  16709  mrieqvlemd  17319  mreexmrid  17333  mreexexlem2d  17335  mreexexlem3d  17336  mreexexlem4d  17337  acsfiindd  18252  tsrdir  18303  f1omvdco2  19037  symgsssg  19056  symggen  19059  lsmunss  19245  efgsfo  19326  lsptpcl  20222  lspun  20230  lsmsp  20329  lspsolvlem  20385  lspsolv  20386  lsppratlem3  20392  lsppratlem4  20393  islbs3  20398  lbsextlem4  20404  aspval2  21083  evlseu  21274  mhpaddcl  21322  clslp  22280  neitr  22312  ordtuni  22322  ordtbas2  22323  ordtbas  22324  ordtrest  22334  cmpcld  22534  comppfsc  22664  1stckgenlem  22685  1stckgen  22686  ptbasfi  22713  fbun  22972  trfil2  23019  isufil2  23040  ufileu  23051  filufint  23052  fmfnfm  23090  hausflim  23113  flimclslem  23116  fclsfnflim  23159  flimfnfcls  23160  alexsubALTlem3  23181  alexsubALTlem4  23182  tsmsgsum  23271  tsmsres  23276  tsmsxplem1  23285  ustund  23354  trust  23362  ustuqtop1  23374  prdsdsf  23501  prdsxmetlem  23502  prdsmet  23504  prdsbl  23628  prdsxmslem2  23666  restmetu  23707  icccmplem2  23967  rrxmval  24550  rrxmet  24553  rrxdstprj1  24554  ovolunlem1  24642  ovolunnul  24645  nulmbl2  24681  volun  24690  volcn  24751  itgsplitioo  24983  limcvallem  25016  limcdif  25021  ellimc2  25022  limcres  25031  limccnp  25036  limccnp2  25037  limcco  25038  dvreslem  25054  dvres2lem  25055  dvaddbr  25083  dvmulbr  25084  lhop2  25160  dvcnvrelem2  25163  elply2  25338  plyf  25340  elplyr  25343  elplyd  25344  ply1term  25346  ply0  25350  plyeq0lem  25352  plyeq0  25353  plyaddlem  25357  plymullem  25358  dgrlem  25371  coeidlem  25379  plyco  25383  plycj  25419  aannenlem2  25470  xrlimcnp  26099  perfectlem2  26359  shlej1  29701  shlub  29755  disjiunel  30914  fcoinver  30925  gsumzresunsn  31293  lsmidl  31568  mxidlprm  31619  lindsun  31685  ordtrestNEW  31850  carsggect  32264  eulerpartlemt  32317  hgt750lemb  32615  hgt750leme  32617  bnj1136  32956  bnj1452  33011  erdszelem8  33139  mclsssvlem  33503  mclsax  33510  mclsind  33511  mthmpps  33523  mclsppslem  33524  xpord2pred  33771  xpord3pred  33777  naddcllem  33810  noextend  33848  ssltun1  33981  ssltun2  33982  lrrecpred  34080  topjoin  34533  poimirlem32  35788  ftc1anclem7  35835  ftc1anc  35837  prdsbnd  35930  rrnequiv  35972  pclfinN  37893  dochdmj1  39383  djhspss  39399  djhunssN  39402  djhlsmcl  39407  dvh4dimlem  39436  dvhdimlem  39437  lclkrlem2c  39502  lclkrlem2v  39521  mapdh9a  39782  hdmapval0  39826  hdmapval3lemN  39830  hdmap10lem  39832  elrfi  40496  cmpfiiin  40499  istopclsd  40502  mzpcompact2lem  40553  eldioph2lem2  40563  eldioph2  40564  rngunsnply  40978  idomsubgmo  41003  dfrcl2  41235  iunrelexp0  41263  relexp0a  41277  brtrclfv2  41288  frege77d  41307  frege109d  41318  frege131d  41325  clsk3nimkb  41603  isotone1  41611  ntrclskb  41632  ntrclsk3  41633  ntrclsk13  41634  ntrneixb  41658  ntrneix3  41660  ntrneix13  41662  infxrpnf  42940  mccllem  43092  limciccioolb  43116  limcicciooub  43132  limcresiooub  43137  limcresioolb  43138  icccncfext  43382  dvnprodlem2  43442  ovolsplit  43483  fourierdlem20  43622  fourierdlem46  43647  fourierdlem48  43649  fourierdlem49  43650  fourierdlem50  43651  fourierdlem51  43652  fourierdlem54  43655  fourierdlem64  43665  fourierdlem76  43677  fourierdlem101  43702  fourierdlem102  43703  fourierdlem103  43704  fourierdlem104  43705  fourierdlem114  43715  sge0resplit  43898  sge0xaddlem1  43925  ismeannd  43959  caragenuncl  44005  omeunle  44008  isomenndlem  44022  hoidmvlelem2  44088  hoidmvlelem3  44089  hoidmvlelem4  44090  perfectALTVlem2  45126