Theorem unssd 4186

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

Syntax hints:   → wi 4   ∧ wa 396   ∪ cun 3946   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-in 3955  df-ss 3965

This theorem is referenced by:  uneqdifeq  4492  tpssi  4839  sofld  6186  unima  6966  fr3nr  7761  ordsuci  7798  sucexeloniOLD  7800  suceloniOLD  7802  xpord2pred  8133  xpord3pred  8140  frrlem13  8285  naddcllem  8677  ralxpmap  8892  marypha1lem  9430  wemapso2lem  9549  unwf  9807  rankunb  9847  ackbij1lem6  10222  ackbij1lem16  10232  ssfin4  10307  isfin1-3  10383  ttukeylem7  10512  fpwwe2lem12  10639  wuncval2  10744  inar1  10772  un0addcl  12509  un0mulcl  12510  ssfzunsnext  13550  fzosplit  13669  fzouzsplit  13671  hashf1lem1  14419  hashf1lem1OLD  14420  ccatrn  14543  trclfvlb3  14962  trclun  14965  relexpfld  15000  saddisj  16410  lcmfunsnlem2lem1  16579  lcmfunsnlem2lem2  16580  lcmfunsnlem2  16581  lcmfun  16586  prmreclem5  16857  4sqlem11  16892  4sqlem19  16900  vdwlem1  16918  vdwlem12  16929  ramub1lem1  16963  ramub1lem2  16964  mrieqvlemd  17577  mreexmrid  17591  mreexexlem2d  17593  mreexexlem3d  17594  mreexexlem4d  17595  acsfiindd  18510  tsrdir  18561  f1omvdco2  19357  symgsssg  19376  symggen  19379  lsmunss  19568  efgsfo  19648  lsptpcl  20734  lspun  20742  lsmsp  20841  lspsolvlem  20900  lspsolv  20901  lsppratlem3  20907  lsppratlem4  20908  islbs3  20913  lbsextlem4  20919  aspval2  21671  evlseu  21865  mhpaddcl  21913  clslp  22872  neitr  22904  ordtuni  22914  ordtbas2  22915  ordtbas  22916  ordtrest  22926  cmpcld  23126  comppfsc  23256  1stckgenlem  23277  1stckgen  23278  ptbasfi  23305  fbun  23564  trfil2  23611  isufil2  23632  ufileu  23643  filufint  23644  fmfnfm  23682  hausflim  23705  flimclslem  23708  fclsfnflim  23751  flimfnfcls  23752  alexsubALTlem3  23773  alexsubALTlem4  23774  tsmsgsum  23863  tsmsres  23868  tsmsxplem1  23877  ustund  23946  trust  23954  ustuqtop1  23966  prdsdsf  24093  prdsxmetlem  24094  prdsmet  24096  prdsbl  24220  prdsxmslem2  24258  restmetu  24299  icccmplem2  24559  rrxmval  25146  rrxmet  25149  rrxdstprj1  25150  ovolunlem1  25238  ovolunnul  25241  nulmbl2  25277  volun  25286  volcn  25347  itgsplitioo  25579  limcvallem  25612  limcdif  25617  ellimc2  25618  limcres  25627  limccnp  25632  limccnp2  25633  limcco  25634  dvreslem  25650  dvres2lem  25651  dvaddbr  25679  dvmulbr  25680  lhop2  25756  dvcnvrelem2  25759  elply2  25934  plyf  25936  elplyr  25939  elplyd  25940  ply1term  25942  ply0  25946  plyeq0lem  25948  plyeq0  25949  plyaddlem  25953  plymullem  25954  dgrlem  25967  coeidlem  25975  plyco  25979  plycj  26015  aannenlem2  26066  xrlimcnp  26697  perfectlem2  26957  noextend  27393  ssltun1  27534  ssltun2  27535  cutlt  27645  lrrecpred  27654  addsproplem2  27680  addsuniflem  27711  negsid  27742  mulsproplem9  27807  ssltmul1  27829  ssltmul2  27830  precsexlem8  27887  precsexlem11  27890  shlej1  30868  shlub  30922  disjiunel  32082  fcoinver  32090  gsumzresunsn  32464  lsmidl  32773  elrspunsn  32809  mxidlprm  32848  qsdrngilem  32870  lindsun  32986  evls1fldgencl  33021  algextdeglem1  33050  algextdeglem2  33051  algextdeglem3  33052  algextdeglem4  33053  algextdeglem5  33054  ordtrestNEW  33187  carsggect  33603  eulerpartlemt  33656  hgt750lemb  33954  hgt750leme  33956  bnj1136  34294  bnj1452  34349  erdszelem8  34475  mclsssvlem  34839  mclsax  34846  mclsind  34847  mthmpps  34859  mclsppslem  34860  gg-dvmulbr  35461  topjoin  35553  poimirlem32  36823  ftc1anclem7  36870  ftc1anc  36872  prdsbnd  36964  rrnequiv  37006  pclfinN  39074  dochdmj1  40564  djhspss  40580  djhunssN  40583  djhlsmcl  40588  dvh4dimlem  40617  dvhdimlem  40618  lclkrlem2c  40683  lclkrlem2v  40702  mapdh9a  40963  hdmapval0  41007  hdmapval3lemN  41011  hdmap10lem  41013  elrfi  41734  cmpfiiin  41737  istopclsd  41740  mzpcompact2lem  41791  eldioph2lem2  41801  eldioph2  41802  rngunsnply  42217  idomsubgmo  42242  omabs2  42384  dfrcl2  42727  iunrelexp0  42755  relexp0a  42769  brtrclfv2  42780  frege77d  42799  frege109d  42810  frege131d  42817  clsk3nimkb  43093  isotone1  43101  ntrclskb  43122  ntrclsk3  43123  ntrclsk13  43124  ntrneixb  43148  ntrneix3  43150  ntrneix13  43152  infxrpnf  44455  pimxrneun  44498  mccllem  44612  limciccioolb  44636  limcicciooub  44652  limcresiooub  44657  limcresioolb  44658  icccncfext  44902  dvnprodlem2  44962  ovolsplit  45003  fourierdlem20  45142  fourierdlem46  45167  fourierdlem48  45169  fourierdlem49  45170  fourierdlem50  45171  fourierdlem51  45172  fourierdlem54  45175  fourierdlem64  45185  fourierdlem76  45197  fourierdlem101  45222  fourierdlem102  45223  fourierdlem103  45224  fourierdlem104  45225  fourierdlem114  45235  sge0resplit  45421  sge0xaddlem1  45448  ismeannd  45482  caragenuncl  45528  omeunle  45531  isomenndlem  45545  hoidmvlelem2  45611  hoidmvlelem3  45612  hoidmvlelem4  45613  perfectALTVlem2  46689  pgindlem  47848