Theorem unssd 4143

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3901   ⊆ wss 3903

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 3438  df-un 3908  df-ss 3920

This theorem is referenced by:  uneqdifeq  4444  tpssi  4789  sofld  6136  unima  6898  fr3nr  7708  ordsuci  7744  resf1extb  7867  resf1ext2b  7868  xpord2pred  8078  xpord3pred  8085  frrlem13  8231  naddcllem  8594  ralxpmap  8823  marypha1lem  9323  wemapso2lem  9444  unwf  9706  rankunb  9746  ackbij1lem6  10118  ackbij1lem16  10128  ssfin4  10204  isfin1-3  10280  ttukeylem7  10409  fpwwe2lem12  10536  wuncval2  10641  inar1  10669  un0addcl  12417  un0mulcl  12418  ssfzunsnext  13472  fzosplit  13595  fzouzsplit  13597  hashf1lem1  14362  ccatrn  14496  trclfvlb3  14918  trclun  14921  relexpfld  14956  saddisj  16376  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  lcmfunsnlem2  16551  lcmfun  16556  prmreclem5  16832  4sqlem11  16867  4sqlem19  16875  vdwlem1  16893  vdwlem12  16904  ramub1lem1  16938  ramub1lem2  16939  mrieqvlemd  17535  mreexmrid  17549  mreexexlem2d  17551  mreexexlem3d  17552  mreexexlem4d  17553  acsfiindd  18459  tsrdir  18510  f1omvdco2  19327  symgsssg  19346  symggen  19349  lsmunss  19538  efgsfo  19618  lsptpcl  20882  lspun  20890  lsmsp  20990  lspsolvlem  21049  lspsolv  21050  lsppratlem3  21056  lsppratlem4  21057  islbs3  21062  lbsextlem4  21068  aspval2  21805  evlseu  21988  mhpaddcl  22036  clslp  23033  neitr  23065  ordtuni  23075  ordtbas2  23076  ordtbas  23077  ordtrest  23087  cmpcld  23287  comppfsc  23417  1stckgenlem  23438  1stckgen  23439  ptbasfi  23466  fbun  23725  trfil2  23772  isufil2  23793  ufileu  23804  filufint  23805  fmfnfm  23843  hausflim  23866  flimclslem  23869  fclsfnflim  23912  flimfnfcls  23913  alexsubALTlem3  23934  alexsubALTlem4  23935  tsmsgsum  24024  tsmsres  24029  tsmsxplem1  24038  ustund  24107  trust  24115  ustuqtop1  24127  prdsdsf  24253  prdsxmetlem  24254  prdsmet  24256  prdsbl  24377  prdsxmslem2  24415  restmetu  24456  icccmplem2  24710  rrxmval  25303  rrxmet  25306  rrxdstprj1  25307  ovolunlem1  25396  ovolunnul  25399  nulmbl2  25435  volun  25444  volcn  25505  itgsplitioo  25737  limcvallem  25770  limcdif  25775  ellimc2  25776  limcres  25785  limccnp  25790  limccnp2  25791  limcco  25792  dvreslem  25808  dvres2lem  25809  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  lhop2  25918  dvcnvrelem2  25921  elply2  26099  plyf  26101  elplyr  26104  elplyd  26105  ply1term  26107  ply0  26111  plyeq0lem  26113  plyeq0  26114  plyaddlem  26118  plymullem  26119  dgrlem  26132  coeidlem  26140  plyco  26144  plycj  26181  plycjOLD  26183  aannenlem2  26235  xrlimcnp  26876  perfectlem2  27139  noextend  27576  ssltun1  27719  ssltun2  27720  cutlt  27845  lrrecpred  27856  addsproplem2  27882  addsuniflem  27913  addsbday  27929  negsid  27952  mulsproplem9  28032  ssltmul1  28055  ssltmul2  28056  precsexlem8  28121  precsexlem11  28124  onaddscl  28179  shlej1  31304  shlub  31358  disjiunel  32540  fcoinver  32548  gsumzresunsn  33009  gsumwun  33018  elrgspnsubrunlem1  33187  elrgspnsubrunlem2  33188  elrgspnsubrun  33189  lsmidl  33338  elrspunsn  33366  mxidlprm  33407  qsdrngilem  33431  lindsun  33592  fldgenfldext  33635  evls1fldgencl  33637  fldextrspunlem1  33642  fldextrspunfld  33643  fldextrspunlem2  33644  fldextrspundgdvdslem  33647  fldextrspundgdvds  33648  algextdeglem1  33684  algextdeglem2  33685  algextdeglem3  33686  algextdeglem4  33687  algextdeglem5  33688  rtelextdg2  33694  constrextdg2lem  33715  constrext2chnlem  33717  constrfiss  33718  constrllcllem  33719  constrlccllem  33720  constrcccllem  33721  ordtrestNEW  33888  carsggect  34286  eulerpartlemt  34339  hgt750lemb  34624  hgt750leme  34626  bnj1136  34964  bnj1452  35019  erdszelem8  35171  mclsssvlem  35535  mclsax  35542  mclsind  35543  mthmpps  35555  mclsppslem  35556  topjoin  36339  weiunse  36442  poimirlem32  37632  ftc1anclem7  37679  ftc1anc  37681  prdsbnd  37773  rrnequiv  37815  pclfinN  39879  dochdmj1  41369  djhspss  41385  djhunssN  41388  djhlsmcl  41393  dvh4dimlem  41422  dvhdimlem  41423  lclkrlem2c  41488  lclkrlem2v  41507  mapdh9a  41768  hdmapval0  41812  hdmapval3lemN  41816  hdmap10lem  41818  deg1gprod  42113  dvun  42332  elrfi  42667  cmpfiiin  42670  istopclsd  42673  mzpcompact2lem  42724  eldioph2lem2  42734  eldioph2  42735  rngunsnply  43142  idomsubgmo  43166  omabs2  43305  dfrcl2  43647  iunrelexp0  43675  relexp0a  43689  brtrclfv2  43700  frege77d  43719  frege109d  43730  frege131d  43737  clsk3nimkb  44013  isotone1  44021  ntrclskb  44042  ntrclsk3  44043  ntrclsk13  44044  ntrneixb  44068  ntrneix3  44070  ntrneix13  44072  infxrpnf  45425  pimxrneun  45467  mccllem  45578  limciccioolb  45602  limcicciooub  45618  limcresiooub  45623  limcresioolb  45624  icccncfext  45868  dvnprodlem2  45928  ovolsplit  45969  fourierdlem20  46108  fourierdlem46  46133  fourierdlem48  46135  fourierdlem49  46136  fourierdlem50  46137  fourierdlem51  46138  fourierdlem54  46141  fourierdlem64  46151  fourierdlem76  46163  fourierdlem101  46188  fourierdlem102  46189  fourierdlem103  46190  fourierdlem104  46191  fourierdlem114  46201  sge0resplit  46387  sge0xaddlem1  46414  ismeannd  46448  caragenuncl  46494  omeunle  46497  isomenndlem  46511  hoidmvlelem2  46577  hoidmvlelem3  46578  hoidmvlelem4  46579  perfectALTVlem2  47706  gpgprismgriedgdmss  48036  pgindlem  49700