Theorem unssd 3751

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

Syntax hints:   → wi 4   ∧ wa 383   ∪ cun 3538   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554

This theorem is referenced by:  uneqdifeq  4009  tpssi  4309  sofld  5500  fr3nr  6871  suceloni  6905  ralxpmap  7793  marypha1lem  8222  wemapso2lem  8340  unwf  8556  rankunb  8596  ackbij1lem6  8930  ackbij1lem16  8940  ssfin4  9015  isfin1-3  9091  ttukeylem7  9220  fpwwe2lem13  9343  wuncval2  9448  inar1  9476  un0addcl  11203  un0mulcl  11204  ssfzunsn  12257  fzosplit  12370  fzouzsplit  12372  hashf1lem1  13096  ccatrn  13225  trclfvlb3  13600  trclun  13603  relexpfld  13637  saddisj  15025  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  lcmfunsnlem2  15191  lcmfun  15196  prmreclem5  15462  4sqlem11  15497  4sqlem19  15505  vdwlem1  15523  vdwlem12  15534  ramub1lem1  15568  ramub1lem2  15569  mrieqvlemd  16112  mreexmrid  16126  mreexexlem2d  16128  mreexexlem3d  16129  mreexexlem4d  16130  acsfiindd  17000  tsrdir  17061  f1omvdco2  17691  symgsssg  17710  symggen  17713  lsmunss  17896  efgsfo  17975  lsptpcl  18800  lspun  18808  lsmsp  18907  lspsolvlem  18963  lspsolv  18964  lsppratlem3  18970  lsppratlem4  18971  islbs3  18976  lbsextlem4  18982  aspval2  19168  evlseu  19337  clslp  20762  neitr  20794  ordtuni  20804  ordtbas2  20805  ordtbas  20806  ordtrest  20816  cmpcld  21015  comppfsc  21145  1stckgenlem  21166  1stckgen  21167  ptbasfi  21194  fbun  21454  trfil2  21501  isufil2  21522  ufileu  21533  filufint  21534  fmfnfm  21572  hausflim  21595  flimclslem  21598  fclsfnflim  21641  flimfnfcls  21642  alexsubALTlem3  21663  alexsubALTlem4  21664  tsmsgsum  21752  tsmsres  21757  tsmsxplem1  21766  ustund  21835  trust  21843  ustuqtop1  21855  prdsdsf  21982  prdsxmetlem  21983  prdsmet  21985  prdsbl  22106  prdsxmslem2  22144  restmetu  22185  icccmplem2  22434  rrxmval  22996  rrxmet  22999  rrxdstprj1  23000  ovolunlem1  23072  ovolunnul  23075  nulmbl2  23111  volun  23120  volcn  23180  itgsplitioo  23410  limcvallem  23441  limcdif  23446  ellimc2  23447  limcres  23456  limccnp  23461  limccnp2  23462  limcco  23463  dvreslem  23479  dvres2lem  23480  dvaddbr  23507  dvmulbr  23508  lhop2  23582  dvcnvrelem2  23585  elply2  23756  plyf  23758  elplyr  23761  elplyd  23762  ply1term  23764  ply0  23768  plyeq0lem  23770  plyeq0  23771  plyaddlem  23775  plymullem  23776  dgrlem  23789  coeidlem  23797  plyco  23801  plycj  23837  aannenlem2  23888  xrlimcnp  24495  perfectlem2  24755  shlej1  27603  shlub  27657  disjiunel  28791  fcoinver  28798  ordtrestNEW  29295  carsggect  29707  eulerpartlemt  29760  bnj1136  30319  bnj1452  30374  erdszelem8  30434  mclsssvlem  30713  mclsax  30720  mclsind  30721  mthmpps  30733  mclsppslem  30734  dftrpred3g  30977  topjoin  31530  poimirlem32  32611  ftc1anclem7  32661  ftc1anc  32663  prdsbnd  32762  rrnequiv  32804  pclfinN  34204  dochdmj1  35697  djhspss  35713  djhunssN  35716  djhlsmcl  35721  dvh4dimlem  35750  dvhdimlem  35751  lclkrlem2c  35816  lclkrlem2v  35835  mapdh9a  36097  hdmapval0  36143  hdmapval3lemN  36147  hdmap10lem  36149  elrfi  36275  cmpfiiin  36278  istopclsd  36281  mzpcompact2lem  36332  eldioph2lem2  36342  eldioph2  36343  rngunsnply  36762  idomsubgmo  36795  dfrcl2  36985  iunrelexp0  37013  relexp0a  37027  brtrclfv2  37038  frege77d  37057  frege109d  37068  frege131d  37075  clsk3nimkb  37358  isotone1  37366  ntrclskb  37387  ntrclsk3  37388  ntrclsk13  37389  ntrneixb  37413  ntrneix3  37415  ntrneix13  37417  unima  38340  mccllem  38664  limciccioolb  38688  limcicciooub  38704  limcresiooub  38709  limcresioolb  38710  icccncfext  38773  dvnprodlem2  38837  ovolsplit  38881  fourierdlem20  39020  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem51  39050  fourierdlem54  39053  fourierdlem64  39063  fourierdlem76  39075  fourierdlem101  39100  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem114  39113  sge0resplit  39299  sge0xaddlem1  39326  ismeannd  39360  caragenuncl  39403  omeunle  39406  isomenndlem  39420  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  perfectALTVlem2  40165