Theorem unssd 4192

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3949   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968

This theorem is referenced by:  uneqdifeq  4493  tpssi  4838  sofld  6207  unima  6984  fr3nr  7792  ordsuci  7828  sucexeloniOLD  7830  suceloniOLD  7832  resf1extb  7956  resf1ext2b  7957  xpord2pred  8170  xpord3pred  8177  frrlem13  8323  naddcllem  8714  ralxpmap  8936  marypha1lem  9473  wemapso2lem  9592  unwf  9850  rankunb  9890  ackbij1lem6  10264  ackbij1lem16  10274  ssfin4  10350  isfin1-3  10426  ttukeylem7  10555  fpwwe2lem12  10682  wuncval2  10787  inar1  10815  un0addcl  12559  un0mulcl  12560  ssfzunsnext  13609  fzosplit  13732  fzouzsplit  13734  hashf1lem1  14494  ccatrn  14627  trclfvlb3  15050  trclun  15053  relexpfld  15088  saddisj  16502  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  lcmfunsnlem2  16677  lcmfun  16682  prmreclem5  16958  4sqlem11  16993  4sqlem19  17001  vdwlem1  17019  vdwlem12  17030  ramub1lem1  17064  ramub1lem2  17065  mrieqvlemd  17672  mreexmrid  17686  mreexexlem2d  17688  mreexexlem3d  17689  mreexexlem4d  17690  acsfiindd  18598  tsrdir  18649  f1omvdco2  19466  symgsssg  19485  symggen  19488  lsmunss  19677  efgsfo  19757  lsptpcl  20977  lspun  20985  lsmsp  21085  lspsolvlem  21144  lspsolv  21145  lsppratlem3  21151  lsppratlem4  21152  islbs3  21157  lbsextlem4  21163  aspval2  21918  evlseu  22107  mhpaddcl  22155  clslp  23156  neitr  23188  ordtuni  23198  ordtbas2  23199  ordtbas  23200  ordtrest  23210  cmpcld  23410  comppfsc  23540  1stckgenlem  23561  1stckgen  23562  ptbasfi  23589  fbun  23848  trfil2  23895  isufil2  23916  ufileu  23927  filufint  23928  fmfnfm  23966  hausflim  23989  flimclslem  23992  fclsfnflim  24035  flimfnfcls  24036  alexsubALTlem3  24057  alexsubALTlem4  24058  tsmsgsum  24147  tsmsres  24152  tsmsxplem1  24161  ustund  24230  trust  24238  ustuqtop1  24250  prdsdsf  24377  prdsxmetlem  24378  prdsmet  24380  prdsbl  24504  prdsxmslem2  24542  restmetu  24583  icccmplem2  24845  rrxmval  25439  rrxmet  25442  rrxdstprj1  25443  ovolunlem1  25532  ovolunnul  25535  nulmbl2  25571  volun  25580  volcn  25641  itgsplitioo  25873  limcvallem  25906  limcdif  25911  ellimc2  25912  limcres  25921  limccnp  25926  limccnp2  25927  limcco  25928  dvreslem  25944  dvres2lem  25945  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  lhop2  26054  dvcnvrelem2  26057  elply2  26235  plyf  26237  elplyr  26240  elplyd  26241  ply1term  26243  ply0  26247  plyeq0lem  26249  plyeq0  26250  plyaddlem  26254  plymullem  26255  dgrlem  26268  coeidlem  26276  plyco  26280  plycj  26317  plycjOLD  26319  aannenlem2  26371  xrlimcnp  27011  perfectlem2  27274  noextend  27711  ssltun1  27853  ssltun2  27854  cutlt  27966  lrrecpred  27977  addsproplem2  28003  addsuniflem  28034  addsbday  28050  negsid  28073  mulsproplem9  28150  ssltmul1  28173  ssltmul2  28174  precsexlem8  28238  precsexlem11  28241  onaddscl  28286  shlej1  31379  shlub  31433  disjiunel  32609  fcoinver  32617  gsumzresunsn  33059  gsumwun  33068  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  elrgspnsubrun  33253  lsmidl  33429  elrspunsn  33457  mxidlprm  33498  qsdrngilem  33522  lindsun  33676  fldgenfldext  33718  evls1fldgencl  33720  fldextrspunlem1  33725  fldextrspunfld  33726  fldextrspunlem2  33727  fldextrspundgdvdslem  33730  fldextrspundgdvds  33731  algextdeglem1  33758  algextdeglem2  33759  algextdeglem3  33760  algextdeglem4  33761  algextdeglem5  33762  rtelextdg2  33768  constrextdg2lem  33789  ordtrestNEW  33920  carsggect  34320  eulerpartlemt  34373  hgt750lemb  34671  hgt750leme  34673  bnj1136  35011  bnj1452  35066  erdszelem8  35203  mclsssvlem  35567  mclsax  35574  mclsind  35575  mthmpps  35587  mclsppslem  35588  topjoin  36366  weiunse  36469  poimirlem32  37659  ftc1anclem7  37706  ftc1anc  37708  prdsbnd  37800  rrnequiv  37842  pclfinN  39902  dochdmj1  41392  djhspss  41408  djhunssN  41411  djhlsmcl  41416  dvh4dimlem  41445  dvhdimlem  41446  lclkrlem2c  41511  lclkrlem2v  41530  mapdh9a  41791  hdmapval0  41835  hdmapval3lemN  41839  hdmap10lem  41841  deg1gprod  42141  dvun  42389  elrfi  42705  cmpfiiin  42708  istopclsd  42711  mzpcompact2lem  42762  eldioph2lem2  42772  eldioph2  42773  rngunsnply  43181  idomsubgmo  43205  omabs2  43345  dfrcl2  43687  iunrelexp0  43715  relexp0a  43729  brtrclfv2  43740  frege77d  43759  frege109d  43770  frege131d  43777  clsk3nimkb  44053  isotone1  44061  ntrclskb  44082  ntrclsk3  44083  ntrclsk13  44084  ntrneixb  44108  ntrneix3  44110  ntrneix13  44112  infxrpnf  45457  pimxrneun  45499  mccllem  45612  limciccioolb  45636  limcicciooub  45652  limcresiooub  45657  limcresioolb  45658  icccncfext  45902  dvnprodlem2  45962  ovolsplit  46003  fourierdlem20  46142  fourierdlem46  46167  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem51  46172  fourierdlem54  46175  fourierdlem64  46185  fourierdlem76  46197  fourierdlem101  46222  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem114  46235  sge0resplit  46421  sge0xaddlem1  46448  ismeannd  46482  caragenuncl  46528  omeunle  46531  isomenndlem  46545  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  perfectALTVlem2  47709  pgindlem  49234