Theorem unssd 4153

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

Syntax hints:   → wi 4   ∧ wa 400   ∪ cun 3911   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930

This theorem is referenced by:  uneqdifeq  4458  tpssi  4807  sofld  6186  unima  6957  fr3nr  7770  ordsuci  7806  resf1extb  7930  resf1ext2b  7931  xpord2pred  8140  xpord3pred  8147  frrlem13  8294  naddcllem  8661  ralxpmap  8893  marypha1lem  9392  wemapso2lem  9513  unwf  9781  rankunb  9821  ackbij1lem6  10206  ackbij1lem16  10216  ssfin4  10293  isfin1-3  10369  ttukeylem7  10498  fpwwe2lem12  10626  wuncval2  10731  inar1  10759  un0addcl  12536  un0mulcl  12537  ssfzunsnext  13596  fzosplit  13720  fzouzsplit  13722  hashf1lem1  14491  ccatrn  14626  trclfvlb3  15047  trclun  15050  relexpfld  15085  saddisj  16522  lcmfunsnlem2lem1  16695  lcmfunsnlem2lem2  16696  lcmfunsnlem2  16697  lcmfun  16702  prmreclem5  16979  4sqlem11  17014  4sqlem19  17022  vdwlem1  17040  vdwlem12  17051  ramub1lem1  17085  ramub1lem2  17086  mrieqvlemd  17684  mreexmrid  17698  mreexexlem2d  17700  mreexexlem3d  17701  mreexexlem4d  17702  acsfiindd  18608  tsrdir  18659  f1omvdco2  19517  symgsssg  19536  symggen  19539  lsmunss  19728  efgsfo  19808  lsptpcl  21077  lspun  21085  lsmsp  21184  lspsolvlem  21243  lspsolv  21244  lsppratlem3  21250  lsppratlem4  21251  islbs3  21256  lbsextlem4  21262  lsmidl  21357  aspval2  22016  evlseu  22202  mhpaddcl  22282  clslp  23273  neitr  23305  ordtuni  23315  ordtbas2  23316  ordtbas  23317  ordtrest  23327  cmpcld  23527  comppfsc  23657  1stckgenlem  23678  1stckgen  23679  ptbasfi  23706  fbun  23965  trfil2  24012  isufil2  24033  ufileu  24044  filufint  24045  fmfnfm  24083  hausflim  24106  flimclslem  24109  fclsfnflim  24152  flimfnfcls  24153  alexsubALTlem3  24174  alexsubALTlem4  24175  tsmsgsum  24264  tsmsres  24269  tsmsxplem1  24278  ustund  24347  trust  24354  ustuqtop1  24366  prdsdsf  24492  prdsxmetlem  24493  prdsmet  24495  prdsbl  24616  prdsxmslem2  24654  restmetu  24695  icccmplem2  24949  rrxmval  25532  rrxmet  25535  rrxdstprj1  25536  ovolunlem1  25624  ovolunnul  25627  nulmbl2  25663  volun  25672  volcn  25733  itgsplitioo  25965  limcvallem  25998  limcdif  26003  ellimc2  26004  limcres  26013  limccnp  26018  limccnp2  26019  limcco  26020  dvreslem  26036  dvres2lem  26037  dvaddbr  26065  dvmulbr  26066  lhop2  26142  dvcnvrelem2  26145  elply2  26321  plyf  26323  elplyr  26326  elplyd  26327  ply1term  26329  ply0  26333  plyeq0lem  26335  plyeq0  26336  plyaddlem  26340  plymullem  26341  dgrlem  26354  coeidlem  26362  plyco  26366  plycj  26402  plycjOLD  26404  aannenlem2  26458  xrlimcnp  27098  perfectlem2  27359  noextend  27795  sltsun1  27946  sltsun2  27947  cutlt  28090  lrrecpred  28102  addsproplem2  28128  addsuniflem  28159  addbday  28176  negsid  28199  mulsproplem9  28282  sltmuls1  28305  sltmuls2  28306  precsexlem8  28372  precsexlem11  28375  onaddscl  28435  bdaypw2n0bndlem  28621  shlej1  31652  shlub  31706  disjiunel  32881  fcoinver  32889  gsumzresunsn  33322  gsumwun  33336  elrgspnsubrunlem1  33507  elrgspnsubrunlem2  33508  elrgspnsubrun  33509  elrspunsn  33680  mxidlprm  33697  qsdrngilem  33720  esplyind  33909  lindsun  33959  fldgenfldext  34002  evls1fldgencl  34004  fldextrspunlem1  34009  fldextrspunfld  34010  fldextrspunlem2  34011  fldextrspundgdvdslem  34014  fldextrspundgdvds  34015  algextdeglem1  34051  algextdeglem2  34052  algextdeglem3  34053  algextdeglem4  34054  algextdeglem5  34055  rtelextdg2  34061  constrextdg2lem  34082  constrext2chnlem  34084  constrfiss  34085  constrllcllem  34086  constrlccllem  34087  constrcccllem  34088  ordtrestNEW  34255  carsggect  34652  eulerpartlemt  34705  hgt750lemb  34987  hgt750leme  34989  bnj1136  35329  bnj1452  35384  erdszelem8  35588  mclsssvlem  35952  mclsax  35959  mclsind  35960  mthmpps  35972  mclsppslem  35973  topjoin  36764  weiunse  36867  poimirlem32  38190  ftc1anclem7  38237  ftc1anc  38239  prdsbnd  38331  rrnequiv  38373  pclfinN  40563  dochdmj1  42053  djhspss  42069  djhunssN  42072  djhlsmcl  42077  dvh4dimlem  42106  dvhdimlem  42107  lclkrlem2c  42172  lclkrlem2v  42191  mapdh9a  42452  hdmapval0  42496  hdmapval3lemN  42500  hdmap10lem  42502  deg1gprod  42796  dvun  43009  elrfi  43316  cmpfiiin  43319  istopclsd  43322  mzpcompact2lem  43373  eldioph2lem2  43383  eldioph2  43384  rngunsnply  43787  idomsubgmo  43811  omabs2  43950  dfrcl2  44291  iunrelexp0  44319  relexp0a  44333  brtrclfv2  44344  frege77d  44363  frege109d  44374  frege131d  44381  clsk3nimkb  44657  isotone1  44665  ntrclskb  44686  ntrclsk3  44687  ntrclsk13  44688  ntrneixb  44712  ntrneix3  44714  ntrneix13  44716  infxrpnf  46051  pimxrneun  46093  mccllem  46204  limciccioolb  46228  limcicciooub  46242  limcresiooub  46247  limcresioolb  46248  icccncfext  46492  dvnprodlem2  46552  ovolsplit  46593  fourierdlem20  46732  fourierdlem46  46757  fourierdlem48  46759  fourierdlem49  46760  fourierdlem50  46761  fourierdlem51  46762  fourierdlem54  46765  fourierdlem64  46775  fourierdlem76  46787  fourierdlem101  46812  fourierdlem102  46813  fourierdlem103  46814  fourierdlem104  46815  fourierdlem114  46825  sge0resplit  47011  sge0xaddlem1  47038  ismeannd  47072  caragenuncl  47118  omeunle  47121  isomenndlem  47135  hoidmvlelem2  47201  hoidmvlelem3  47202  hoidmvlelem4  47203  perfectALTVlem2  48375  gpgprismgriedgdmss  48705  pgindlem  50377