Theorem unssd 4189

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3896   ∪ cun 4148

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-un 4150

This theorem is used by:  uneqdifeq  4447  tpssi  4792  sofld  6181  unima  6965  fr3nr  7790  ordsuci  7826  resf1extb  7950  resf1ext2b  7951  xpord2pred  8169  xpord3pred  8176  frrlem13  8324  naddcllem  8693  ralxpmap  8932  marypha1lem  9432  wemapso2lem  9553  unwf  9825  rankunb  9871  ackbij1lem6  10309  ackbij1lem16  10319  ssfin4  10395  isfin1-3  10471  ttukeylem7  10600  fpwwe2lem12  10734  wuncval2  10839  inar1  10867  un0addcl  12646  un0mulcl  12647  ssfzunsnext  13710  fzosplit  13834  fzouzsplit  13836  hashf1lem1  14607  ccatrn  14742  trclfvlb3  15173  trclun  15176  relexpfld  15211  saddisj  16644  lcmfunsnlem2lem1  16822  lcmfunsnlem2lem2  16823  lcmfunsnlem2  16824  lcmfun  16829  prmreclem5  17107  4sqlem11  17142  4sqlem19  17150  vdwlem1  17168  vdwlem12  17179  ramub1lem1  17213  ramub1lem2  17214  mrieqvlemd  17812  mreexmrid  17826  mreexexlem2d  17828  mreexexlem3d  17829  mreexexlem4d  17830  acsfiindd  18736  tsrdir  18787  f1omvdco2  19671  symgsssg  19690  symggen  19693  lsmunss  19882  efgsfo  19962  lsptpcl  21263  lspun  21271  lsmsp  21370  lspsolvlem  21429  lspsolv  21430  lsppratlem3  21436  lsppratlem4  21437  islbs3  21442  lbsextlem4  21448  lsmidl  21547  aspval2  22215  evlseu  22401  mhpaddcl  22481  clslp  23475  neitr  23507  ordtuni  23517  ordtbas2  23518  ordtbas  23519  ordtrest  23529  cmpcld  23729  comppfsc  23860  1stckgenlem  23881  1stckgen  23882  ptbasfi  23909  fbun  24168  trfil2  24215  isufil2  24236  ufileu  24247  filufint  24248  fmfnfm  24286  hausflim  24309  flimclslem  24312  fclsfnflim  24355  flimfnfcls  24356  alexsubALTlem3  24377  alexsubALTlem4  24378  tsmsgsum  24467  tsmsres  24472  tsmsxplem1  24481  ustund  24550  trust  24557  ustuqtop1  24569  prdsdsf  24695  prdsxmetlem  24696  prdsmet  24698  prdsbl  24819  prdsxmslem2  24857  restmetu  24898  icccmplem2  25152  rrxmval  25735  rrxmet  25738  rrxdstprj1  25739  ovolunlem1  25827  ovolunnul  25830  nulmbl2  25866  volun  25875  volcn  25936  itgsplitioo  26167  limcvallem  26200  limcdif  26205  ellimc2  26206  limcres  26215  limccnp  26220  limccnp2  26221  limcco  26222  dvreslem  26238  dvres2lem  26239  dvaddbr  26267  dvmulbr  26268  lhop2  26344  dvcnvrelem2  26347  elply2  26523  plyf  26525  elplyr  26528  elplyd  26529  ply1term  26531  ply0  26535  plyeq0lem  26538  plyeq0  26539  plyaddlem  26543  plymullem  26544  dgrlem  26557  coeidlem  26565  plyco  26569  plycj  26605  aannenlem2  26665  xrlimcnp  27305  perfectlem2  27566  noextend  28032  sltsun1  28183  sltsun2  28184  cutlt  28327  lrrecpred  28339  addsproplem2  28365  addsuniflem  28396  addbday  28413  negsid  28436  mulsproplem9  28519  sltmuls1  28542  sltmuls2  28543  precsexlem8  28609  precsexlem11  28612  onaddscl  28672  bdaypw2n0bndlem  28858  shlej1  31971  shlub  32025  disjiunel  33241  fcoinver  33249  gsumzresunsn  33673  gsumwun  33687  elrgspnsubrunlem1  33858  elrgspnsubrunlem2  33859  elrgspnsubrun  33860  elrspunsn  34029  mxidlprm  34045  qsdrngilem  34068  esplyind  34257  lindsun  34307  fldgenfldext  34350  evls1fldgencl  34352  fldextrspunlem1  34357  fldextrspunfld  34358  fldextrspunlem2  34359  fldextrspundgdvdslem  34362  fldextrspundgdvds  34363  algextdeglem1  34399  algextdeglem2  34400  algextdeglem3  34401  algextdeglem4  34402  algextdeglem5  34403  rtelextdg2  34409  constrextdg2lem  34430  constrext2chnlem  34432  constrfiss  34433  constrllcllem  34434  constrlccllem  34435  constrcccllem  34436  ordtrestNEW  34603  carsggect  35000  eulerpartlemt  35053  hgt750lemb  35335  hgt750leme  35337  bnj1136  35677  bnj1452  35732  erdszelem8  36081  mclsssvlem  36445  mclsax  36452  mclsind  36453  mthmpps  36465  mclsppslem  36466  topjoin  37277  weiunse  37380  poimirlem32  38707  ftc1anclem7  38754  ftc1anc  38756  prdsbnd  38864  rrnequiv  38906  pclfinN  41094  dochdmj1  42584  djhspss  42600  djhunssN  42603  djhlsmcl  42608  dvh4dimlem  42637  dvhdimlem  42638  lclkrlem2c  42703  lclkrlem2v  42722  mapdh9a  42983  hdmapval0  43027  hdmapval3lemN  43031  hdmap10lem  43033  deg1gprod  43327  dvun  43547  elrfi  43842  cmpfiiin  43845  istopclsd  43848  mzpcompact2lem  43899  eldioph2lem2  43909  eldioph2  43910  rngunsnply  44308  idomsubgmo  44332  omabs2  44471  dfrcl2  44811  iunrelexp0  44839  relexp0a  44853  brtrclfv2  44864  frege77d  44883  frege109d  44894  frege131d  44901  clsk3nimkb  45177  isotone1  45185  ntrclskb  45206  ntrclsk3  45207  ntrclsk13  45208  ntrneixb  45232  ntrneix3  45234  ntrneix13  45236  infxrpnf  46592  pimxrneun  46634  mccllem  46745  limciccioolb  46769  limcicciooub  46783  limcresiooub  46788  limcresioolb  46789  icccncfext  47033  dvnprodlem2  47093  ovolsplit  47134  fourierdlem20  47273  fourierdlem46  47298  fourierdlem48  47300  fourierdlem49  47301  fourierdlem50  47302  fourierdlem51  47303  fourierdlem54  47306  fourierdlem64  47316  fourierdlem76  47328  fourierdlem101  47353  fourierdlem102  47354  fourierdlem103  47355  fourierdlem104  47356  fourierdlem114  47366  sge0resplit  47552  sge0xaddlem1  47579  ismeannd  47613  caragenuncl  47659  omeunle  47662  isomenndlem  47676  hoidmvlelem2  47742  hoidmvlelem3  47743  hoidmvlelem4  47744  perfectALTVlem2  48956  gpgprismgriedgdmss  49286  pgindlem  51019