Theorem unssd 4126

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

Syntax hints:   → wi 4   ∧ wa 397   ∪ cun 3890   ⊆ wss 3892

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-un 3897  df-in 3899  df-ss 3909

This theorem is referenced by:  uneqdifeq  4429  tpssi  4775  sofld  6105  unima  6875  fr3nr  7654  sucexeloni  7690  suceloniOLD  7692  frrlem13  8145  ralxpmap  8715  marypha1lem  9236  wemapso2lem  9355  unwf  9612  rankunb  9652  ackbij1lem6  10027  ackbij1lem16  10037  ssfin4  10112  isfin1-3  10188  ttukeylem7  10317  fpwwe2lem12  10444  wuncval2  10549  inar1  10577  un0addcl  12312  un0mulcl  12313  ssfzunsnext  13347  fzosplit  13466  fzouzsplit  13468  hashf1lem1  14213  hashf1lem1OLD  14214  ccatrn  14339  trclfvlb3  14767  trclun  14770  relexpfld  14805  saddisj  16217  lcmfunsnlem2lem1  16388  lcmfunsnlem2lem2  16389  lcmfunsnlem2  16390  lcmfun  16395  prmreclem5  16666  4sqlem11  16701  4sqlem19  16709  vdwlem1  16727  vdwlem12  16738  ramub1lem1  16772  ramub1lem2  16773  mrieqvlemd  17383  mreexmrid  17397  mreexexlem2d  17399  mreexexlem3d  17400  mreexexlem4d  17401  acsfiindd  18316  tsrdir  18367  f1omvdco2  19101  symgsssg  19120  symggen  19123  lsmunss  19309  efgsfo  19390  lsptpcl  20286  lspun  20294  lsmsp  20393  lspsolvlem  20449  lspsolv  20450  lsppratlem3  20456  lsppratlem4  20457  islbs3  20462  lbsextlem4  20468  aspval2  21147  evlseu  21338  mhpaddcl  21386  clslp  22344  neitr  22376  ordtuni  22386  ordtbas2  22387  ordtbas  22388  ordtrest  22398  cmpcld  22598  comppfsc  22728  1stckgenlem  22749  1stckgen  22750  ptbasfi  22777  fbun  23036  trfil2  23083  isufil2  23104  ufileu  23115  filufint  23116  fmfnfm  23154  hausflim  23177  flimclslem  23180  fclsfnflim  23223  flimfnfcls  23224  alexsubALTlem3  23245  alexsubALTlem4  23246  tsmsgsum  23335  tsmsres  23340  tsmsxplem1  23349  ustund  23418  trust  23426  ustuqtop1  23438  prdsdsf  23565  prdsxmetlem  23566  prdsmet  23568  prdsbl  23692  prdsxmslem2  23730  restmetu  23771  icccmplem2  24031  rrxmval  24614  rrxmet  24617  rrxdstprj1  24618  ovolunlem1  24706  ovolunnul  24709  nulmbl2  24745  volun  24754  volcn  24815  itgsplitioo  25047  limcvallem  25080  limcdif  25085  ellimc2  25086  limcres  25095  limccnp  25100  limccnp2  25101  limcco  25102  dvreslem  25118  dvres2lem  25119  dvaddbr  25147  dvmulbr  25148  lhop2  25224  dvcnvrelem2  25227  elply2  25402  plyf  25404  elplyr  25407  elplyd  25408  ply1term  25410  ply0  25414  plyeq0lem  25416  plyeq0  25417  plyaddlem  25421  plymullem  25422  dgrlem  25435  coeidlem  25443  plyco  25447  plycj  25483  aannenlem2  25534  xrlimcnp  26163  perfectlem2  26423  shlej1  29767  shlub  29821  disjiunel  30980  fcoinver  30991  gsumzresunsn  31359  lsmidl  31634  mxidlprm  31685  lindsun  31751  ordtrestNEW  31916  carsggect  32330  eulerpartlemt  32383  hgt750lemb  32681  hgt750leme  32683  bnj1136  33022  bnj1452  33077  erdszelem8  33205  mclsssvlem  33569  mclsax  33576  mclsind  33577  mthmpps  33589  mclsppslem  33590  xpord2pred  33837  xpord3pred  33843  naddcllem  33876  noextend  33914  ssltun1  34047  ssltun2  34048  lrrecpred  34146  topjoin  34599  poimirlem32  35853  ftc1anclem7  35900  ftc1anc  35902  prdsbnd  35995  rrnequiv  36037  pclfinN  37956  dochdmj1  39446  djhspss  39462  djhunssN  39465  djhlsmcl  39470  dvh4dimlem  39499  dvhdimlem  39500  lclkrlem2c  39565  lclkrlem2v  39584  mapdh9a  39845  hdmapval0  39889  hdmapval3lemN  39893  hdmap10lem  39895  elrfi  40553  cmpfiiin  40556  istopclsd  40559  mzpcompact2lem  40610  eldioph2lem2  40620  eldioph2  40621  rngunsnply  41036  idomsubgmo  41061  dfrcl2  41320  iunrelexp0  41348  relexp0a  41362  brtrclfv2  41373  frege77d  41392  frege109d  41403  frege131d  41410  clsk3nimkb  41688  isotone1  41696  ntrclskb  41717  ntrclsk3  41718  ntrclsk13  41719  ntrneixb  41743  ntrneix3  41745  ntrneix13  41747  infxrpnf  43034  pimxrneun  43077  mccllem  43187  limciccioolb  43211  limcicciooub  43227  limcresiooub  43232  limcresioolb  43233  icccncfext  43477  dvnprodlem2  43537  ovolsplit  43578  fourierdlem20  43717  fourierdlem46  43742  fourierdlem48  43744  fourierdlem49  43745  fourierdlem50  43746  fourierdlem51  43747  fourierdlem54  43750  fourierdlem64  43760  fourierdlem76  43772  fourierdlem101  43797  fourierdlem102  43798  fourierdlem103  43799  fourierdlem104  43800  fourierdlem114  43810  sge0resplit  43994  sge0xaddlem1  44021  ismeannd  44055  caragenuncl  44101  omeunle  44104  isomenndlem  44118  hoidmvlelem2  44184  hoidmvlelem3  44185  hoidmvlelem4  44186  perfectALTVlem2  45232