Theorem unssd 4045

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

Syntax hints:   → wi 4   ∧ wa 387   ∪ cun 3822   ⊆ wss 3824

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-v 3412  df-un 3829  df-in 3831  df-ss 3838

This theorem is referenced by:  uneqdifeq  4316  tpssi  4640  sofld  5882  fr3nr  7309  suceloni  7343  ralxpmap  8257  marypha1lem  8691  wemapso2lem  8810  unwf  9032  rankunb  9072  ackbij1lem6  9444  ackbij1lem16  9454  ssfin4  9529  isfin1-3  9605  ttukeylem7  9734  fpwwe2lem13  9861  wuncval2  9966  inar1  9994  un0addcl  11741  un0mulcl  11742  ssfzunsnext  12767  fzosplit  12884  fzouzsplit  12886  hashf1lem1  13625  ccatrn  13751  trclfvlb3  14231  trclun  14234  relexpfld  14268  saddisj  15673  lcmfunsnlem2lem1  15837  lcmfunsnlem2lem2  15838  lcmfunsnlem2  15839  lcmfun  15844  prmreclem5  16111  4sqlem11  16146  4sqlem19  16154  vdwlem1  16172  vdwlem12  16183  ramub1lem1  16217  ramub1lem2  16218  mrieqvlemd  16771  mreexmrid  16785  mreexexlem2d  16787  mreexexlem3d  16788  mreexexlem4d  16789  acsfiindd  17658  tsrdir  17719  f1omvdco2  18350  symgsssg  18369  symggen  18372  lsmunss  18557  efgsfo  18637  lsptpcl  19486  lspun  19494  lsmsp  19593  lspsolvlem  19649  lspsolv  19650  lsppratlem3  19656  lsppratlem4  19657  islbs3  19662  lbsextlem4  19668  aspval2  19854  evlseu  20022  mhpaddcl  20057  clslp  21476  neitr  21508  ordtuni  21518  ordtbas2  21519  ordtbas  21520  ordtrest  21530  cmpcld  21730  comppfsc  21860  1stckgenlem  21881  1stckgen  21882  ptbasfi  21909  fbun  22168  trfil2  22215  isufil2  22236  ufileu  22247  filufint  22248  fmfnfm  22286  hausflim  22309  flimclslem  22312  fclsfnflim  22355  flimfnfcls  22356  alexsubALTlem3  22377  alexsubALTlem4  22378  tsmsgsum  22466  tsmsres  22471  tsmsxplem1  22480  ustund  22549  trust  22557  ustuqtop1  22569  prdsdsf  22696  prdsxmetlem  22697  prdsmet  22699  prdsbl  22820  prdsxmslem2  22858  restmetu  22899  icccmplem2  23150  rrxmval  23727  rrxmet  23730  rrxdstprj1  23731  ovolunlem1  23817  ovolunnul  23820  nulmbl2  23856  volun  23865  volcn  23926  itgsplitioo  24157  limcvallem  24188  limcdif  24193  ellimc2  24194  limcres  24203  limccnp  24208  limccnp2  24209  limcco  24210  dvreslem  24226  dvres2lem  24227  dvaddbr  24254  dvmulbr  24255  lhop2  24331  dvcnvrelem2  24334  elply2  24505  plyf  24507  elplyr  24510  elplyd  24511  ply1term  24513  ply0  24517  plyeq0lem  24519  plyeq0  24520  plyaddlem  24524  plymullem  24525  dgrlem  24538  coeidlem  24546  plyco  24550  plycj  24586  aannenlem2  24637  xrlimcnp  25264  perfectlem2  25524  shlej1  28934  shlub  28988  disjiunel  30130  fcoinver  30139  lindsun  30683  ordtrestNEW  30841  carsggect  31254  eulerpartlemt  31307  hgt750lemb  31608  hgt750leme  31610  bnj1136  31947  bnj1452  32002  erdszelem8  32063  mclsssvlem  32362  mclsax  32369  mclsind  32370  mthmpps  32382  mclsppslem  32383  dftrpred3g  32626  frrlem13  32689  noextend  32727  ssltun1  32823  ssltun2  32824  topjoin  33267  poimirlem32  34398  ftc1anclem7  34447  ftc1anc  34449  prdsbnd  34546  rrnequiv  34588  pclfinN  36514  dochdmj1  38004  djhspss  38020  djhunssN  38023  djhlsmcl  38028  dvh4dimlem  38057  dvhdimlem  38058  lclkrlem2c  38123  lclkrlem2v  38142  mapdh9a  38403  hdmapval0  38447  hdmapval3lemN  38451  hdmap10lem  38453  elrfi  38720  cmpfiiin  38723  istopclsd  38726  mzpcompact2lem  38777  eldioph2lem2  38787  eldioph2  38788  rngunsnply  39203  idomsubgmo  39228  dfrcl2  39416  iunrelexp0  39444  relexp0a  39458  brtrclfv2  39469  frege77d  39488  frege109d  39499  frege131d  39506  clsk3nimkb  39787  isotone1  39795  ntrclskb  39816  ntrclsk3  39817  ntrclsk13  39818  ntrneixb  39842  ntrneix3  39844  ntrneix13  39846  unima  40877  infxrpnf  41182  mccllem  41339  limciccioolb  41363  limcicciooub  41379  limcresiooub  41384  limcresioolb  41385  icccncfext  41630  dvnprodlem2  41692  ovolsplit  41734  fourierdlem20  41873  fourierdlem46  41898  fourierdlem48  41900  fourierdlem49  41901  fourierdlem50  41902  fourierdlem51  41903  fourierdlem54  41906  fourierdlem64  41916  fourierdlem76  41928  fourierdlem101  41953  fourierdlem102  41954  fourierdlem103  41955  fourierdlem104  41956  fourierdlem114  41966  sge0resplit  42149  sge0xaddlem1  42176  ismeannd  42210  caragenuncl  42256  omeunle  42259  isomenndlem  42273  hoidmvlelem2  42339  hoidmvlelem3  42340  hoidmvlelem4  42341  perfectALTVlem2  43285