Theorem unssd 4151

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3909   ⊆ wss 3911

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-ss 3928

This theorem is referenced by:  uneqdifeq  4452  tpssi  4798  sofld  6148  unima  6918  fr3nr  7728  ordsuci  7764  sucexeloniOLD  7766  resf1extb  7890  resf1ext2b  7891  xpord2pred  8101  xpord3pred  8108  frrlem13  8254  naddcllem  8617  ralxpmap  8846  marypha1lem  9360  wemapso2lem  9481  unwf  9739  rankunb  9779  ackbij1lem6  10153  ackbij1lem16  10163  ssfin4  10239  isfin1-3  10315  ttukeylem7  10444  fpwwe2lem12  10571  wuncval2  10676  inar1  10704  un0addcl  12451  un0mulcl  12452  ssfzunsnext  13506  fzosplit  13629  fzouzsplit  13631  hashf1lem1  14396  ccatrn  14530  trclfvlb3  14953  trclun  14956  relexpfld  14991  saddisj  16411  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  lcmfunsnlem2  16586  lcmfun  16591  prmreclem5  16867  4sqlem11  16902  4sqlem19  16910  vdwlem1  16928  vdwlem12  16939  ramub1lem1  16973  ramub1lem2  16974  mrieqvlemd  17566  mreexmrid  17580  mreexexlem2d  17582  mreexexlem3d  17583  mreexexlem4d  17584  acsfiindd  18488  tsrdir  18539  f1omvdco2  19354  symgsssg  19373  symggen  19376  lsmunss  19565  efgsfo  19645  lsptpcl  20861  lspun  20869  lsmsp  20969  lspsolvlem  21028  lspsolv  21029  lsppratlem3  21035  lsppratlem4  21036  islbs3  21041  lbsextlem4  21047  aspval2  21783  evlseu  21966  mhpaddcl  22014  clslp  23011  neitr  23043  ordtuni  23053  ordtbas2  23054  ordtbas  23055  ordtrest  23065  cmpcld  23265  comppfsc  23395  1stckgenlem  23416  1stckgen  23417  ptbasfi  23444  fbun  23703  trfil2  23750  isufil2  23771  ufileu  23782  filufint  23783  fmfnfm  23821  hausflim  23844  flimclslem  23847  fclsfnflim  23890  flimfnfcls  23891  alexsubALTlem3  23912  alexsubALTlem4  23913  tsmsgsum  24002  tsmsres  24007  tsmsxplem1  24016  ustund  24085  trust  24093  ustuqtop1  24105  prdsdsf  24231  prdsxmetlem  24232  prdsmet  24234  prdsbl  24355  prdsxmslem2  24393  restmetu  24434  icccmplem2  24688  rrxmval  25281  rrxmet  25284  rrxdstprj1  25285  ovolunlem1  25374  ovolunnul  25377  nulmbl2  25413  volun  25422  volcn  25483  itgsplitioo  25715  limcvallem  25748  limcdif  25753  ellimc2  25754  limcres  25763  limccnp  25768  limccnp2  25769  limcco  25770  dvreslem  25786  dvres2lem  25787  dvaddbr  25816  dvmulbr  25817  dvmulbrOLD  25818  lhop2  25896  dvcnvrelem2  25899  elply2  26077  plyf  26079  elplyr  26082  elplyd  26083  ply1term  26085  ply0  26089  plyeq0lem  26091  plyeq0  26092  plyaddlem  26096  plymullem  26097  dgrlem  26110  coeidlem  26118  plyco  26122  plycj  26159  plycjOLD  26161  aannenlem2  26213  xrlimcnp  26854  perfectlem2  27117  noextend  27554  ssltun1  27696  ssltun2  27697  cutlt  27816  lrrecpred  27827  addsproplem2  27853  addsuniflem  27884  addsbday  27900  negsid  27923  mulsproplem9  28003  ssltmul1  28026  ssltmul2  28027  precsexlem8  28092  precsexlem11  28095  onaddscl  28150  shlej1  31262  shlub  31316  disjiunel  32498  fcoinver  32506  gsumzresunsn  32969  gsumwun  32978  elrgspnsubrunlem1  33171  elrgspnsubrunlem2  33172  elrgspnsubrun  33173  lsmidl  33345  elrspunsn  33373  mxidlprm  33414  qsdrngilem  33438  lindsun  33594  fldgenfldext  33636  evls1fldgencl  33638  fldextrspunlem1  33643  fldextrspunfld  33644  fldextrspunlem2  33645  fldextrspundgdvdslem  33648  fldextrspundgdvds  33649  algextdeglem1  33680  algextdeglem2  33681  algextdeglem3  33682  algextdeglem4  33683  algextdeglem5  33684  rtelextdg2  33690  constrextdg2lem  33711  constrext2chnlem  33713  constrfiss  33714  constrllcllem  33715  constrlccllem  33716  constrcccllem  33717  ordtrestNEW  33884  carsggect  34282  eulerpartlemt  34335  hgt750lemb  34620  hgt750leme  34622  bnj1136  34960  bnj1452  35015  erdszelem8  35158  mclsssvlem  35522  mclsax  35529  mclsind  35530  mthmpps  35542  mclsppslem  35543  topjoin  36326  weiunse  36429  poimirlem32  37619  ftc1anclem7  37666  ftc1anc  37668  prdsbnd  37760  rrnequiv  37802  pclfinN  39867  dochdmj1  41357  djhspss  41373  djhunssN  41376  djhlsmcl  41381  dvh4dimlem  41410  dvhdimlem  41411  lclkrlem2c  41476  lclkrlem2v  41495  mapdh9a  41756  hdmapval0  41800  hdmapval3lemN  41804  hdmap10lem  41806  deg1gprod  42101  dvun  42320  elrfi  42655  cmpfiiin  42658  istopclsd  42661  mzpcompact2lem  42712  eldioph2lem2  42722  eldioph2  42723  rngunsnply  43131  idomsubgmo  43155  omabs2  43294  dfrcl2  43636  iunrelexp0  43664  relexp0a  43678  brtrclfv2  43689  frege77d  43708  frege109d  43719  frege131d  43726  clsk3nimkb  44002  isotone1  44010  ntrclskb  44031  ntrclsk3  44032  ntrclsk13  44033  ntrneixb  44057  ntrneix3  44059  ntrneix13  44061  infxrpnf  45415  pimxrneun  45457  mccllem  45568  limciccioolb  45592  limcicciooub  45608  limcresiooub  45613  limcresioolb  45614  icccncfext  45858  dvnprodlem2  45918  ovolsplit  45959  fourierdlem20  46098  fourierdlem46  46123  fourierdlem48  46125  fourierdlem49  46126  fourierdlem50  46127  fourierdlem51  46128  fourierdlem54  46131  fourierdlem64  46141  fourierdlem76  46153  fourierdlem101  46178  fourierdlem102  46179  fourierdlem103  46180  fourierdlem104  46181  fourierdlem114  46191  sge0resplit  46377  sge0xaddlem1  46404  ismeannd  46438  caragenuncl  46484  omeunle  46487  isomenndlem  46501  hoidmvlelem2  46567  hoidmvlelem3  46568  hoidmvlelem4  46569  perfectALTVlem2  47696  gpgprismgriedgdmss  48016  pgindlem  49677