Theorem unssd 4145

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

Syntax hints:   → wi 4   ∧ wa 400   ∪ cun 3903   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922

This theorem is referenced by:  uneqdifeq  4453  tpssi  4803  sofld  6185  unima  6956  fr3nr  7767  ordsuci  7803  resf1extb  7927  resf1ext2b  7928  xpord2pred  8137  xpord3pred  8144  frrlem13  8291  naddcllem  8658  ralxpmap  8890  marypha1lem  9389  wemapso2lem  9510  unwf  9778  rankunb  9818  ackbij1lem6  10203  ackbij1lem16  10213  ssfin4  10289  isfin1-3  10365  ttukeylem7  10494  fpwwe2lem12  10622  wuncval2  10727  inar1  10755  un0addcl  12532  un0mulcl  12533  ssfzunsnext  13593  fzosplit  13717  fzouzsplit  13719  hashf1lem1  14488  ccatrn  14623  trclfvlb3  15044  trclun  15047  relexpfld  15082  saddisj  16518  lcmfunsnlem2lem1  16691  lcmfunsnlem2lem2  16692  lcmfunsnlem2  16693  lcmfun  16698  prmreclem5  16975  4sqlem11  17010  4sqlem19  17018  vdwlem1  17036  vdwlem12  17047  ramub1lem1  17081  ramub1lem2  17082  mrieqvlemd  17680  mreexmrid  17694  mreexexlem2d  17696  mreexexlem3d  17697  mreexexlem4d  17698  acsfiindd  18604  tsrdir  18655  f1omvdco2  19513  symgsssg  19532  symggen  19535  lsmunss  19724  efgsfo  19804  lsptpcl  21100  lspun  21108  lsmsp  21207  lspsolvlem  21266  lspsolv  21267  lsppratlem3  21273  lsppratlem4  21274  islbs3  21279  lbsextlem4  21285  lsmidl  21384  aspval2  22048  evlseu  22234  mhpaddcl  22314  clslp  23305  neitr  23337  ordtuni  23347  ordtbas2  23348  ordtbas  23349  ordtrest  23359  cmpcld  23559  comppfsc  23689  1stckgenlem  23710  1stckgen  23711  ptbasfi  23738  fbun  23997  trfil2  24044  isufil2  24065  ufileu  24076  filufint  24077  fmfnfm  24115  hausflim  24138  flimclslem  24141  fclsfnflim  24184  flimfnfcls  24185  alexsubALTlem3  24206  alexsubALTlem4  24207  tsmsgsum  24296  tsmsres  24301  tsmsxplem1  24310  ustund  24379  trust  24386  ustuqtop1  24398  prdsdsf  24524  prdsxmetlem  24525  prdsmet  24527  prdsbl  24648  prdsxmslem2  24686  restmetu  24727  icccmplem2  24981  rrxmval  25564  rrxmet  25567  rrxdstprj1  25568  ovolunlem1  25656  ovolunnul  25659  nulmbl2  25695  volun  25704  volcn  25765  itgsplitioo  25997  limcvallem  26030  limcdif  26035  ellimc2  26036  limcres  26045  limccnp  26050  limccnp2  26051  limcco  26052  dvreslem  26068  dvres2lem  26069  dvaddbr  26097  dvmulbr  26098  lhop2  26174  dvcnvrelem2  26177  elply2  26353  plyf  26355  elplyr  26358  elplyd  26359  ply1term  26361  ply0  26365  plyeq0lem  26367  plyeq0  26368  plyaddlem  26372  plymullem  26373  dgrlem  26386  coeidlem  26394  plyco  26398  plycj  26434  plycjOLD  26436  aannenlem2  26492  xrlimcnp  27133  perfectlem2  27394  noextend  27830  sltsun1  27981  sltsun2  27982  cutlt  28125  lrrecpred  28137  addsproplem2  28163  addsuniflem  28194  addbday  28211  negsid  28234  mulsproplem9  28317  sltmuls1  28340  sltmuls2  28341  precsexlem8  28407  precsexlem11  28410  onaddscl  28470  bdaypw2n0bndlem  28656  shlej1  31712  shlub  31766  disjiunel  32941  fcoinver  32949  gsumzresunsn  33382  gsumwun  33396  elrgspnsubrunlem1  33567  elrgspnsubrunlem2  33568  elrgspnsubrun  33569  elrspunsn  33737  mxidlprm  33753  qsdrngilem  33776  esplyind  33965  lindsun  34015  fldgenfldext  34058  evls1fldgencl  34060  fldextrspunlem1  34065  fldextrspunfld  34066  fldextrspunlem2  34067  fldextrspundgdvdslem  34070  fldextrspundgdvds  34071  algextdeglem1  34107  algextdeglem2  34108  algextdeglem3  34109  algextdeglem4  34110  algextdeglem5  34111  rtelextdg2  34117  constrextdg2lem  34138  constrext2chnlem  34140  constrfiss  34141  constrllcllem  34142  constrlccllem  34143  constrcccllem  34144  ordtrestNEW  34311  carsggect  34708  eulerpartlemt  34761  hgt750lemb  35043  hgt750leme  35045  bnj1136  35385  bnj1452  35440  erdszelem8  35690  mclsssvlem  36054  mclsax  36061  mclsind  36062  mthmpps  36074  mclsppslem  36075  topjoin  36876  weiunse  36979  poimirlem32  38303  ftc1anclem7  38350  ftc1anc  38352  prdsbnd  38444  rrnequiv  38486  pclfinN  40674  dochdmj1  42164  djhspss  42180  djhunssN  42183  djhlsmcl  42188  dvh4dimlem  42217  dvhdimlem  42218  lclkrlem2c  42283  lclkrlem2v  42302  mapdh9a  42563  hdmapval0  42607  hdmapval3lemN  42611  hdmap10lem  42613  deg1gprod  42907  dvun  43120  elrfi  43425  cmpfiiin  43428  istopclsd  43431  mzpcompact2lem  43482  eldioph2lem2  43492  eldioph2  43493  rngunsnply  43896  idomsubgmo  43920  omabs2  44059  dfrcl2  44400  iunrelexp0  44428  relexp0a  44442  brtrclfv2  44453  frege77d  44472  frege109d  44483  frege131d  44490  clsk3nimkb  44766  isotone1  44774  ntrclskb  44795  ntrclsk3  44796  ntrclsk13  44797  ntrneixb  44821  ntrneix3  44823  ntrneix13  44825  infxrpnf  46160  pimxrneun  46202  mccllem  46313  limciccioolb  46337  limcicciooub  46351  limcresiooub  46356  limcresioolb  46357  icccncfext  46601  dvnprodlem2  46661  ovolsplit  46702  fourierdlem20  46841  fourierdlem46  46866  fourierdlem48  46868  fourierdlem49  46869  fourierdlem50  46870  fourierdlem51  46871  fourierdlem54  46874  fourierdlem64  46884  fourierdlem76  46896  fourierdlem101  46921  fourierdlem102  46922  fourierdlem103  46923  fourierdlem104  46924  fourierdlem114  46934  sge0resplit  47120  sge0xaddlem1  47147  ismeannd  47181  caragenuncl  47227  omeunle  47230  isomenndlem  47244  hoidmvlelem2  47310  hoidmvlelem3  47311  hoidmvlelem4  47312  perfectALTVlem2  48487  gpgprismgriedgdmss  48817  pgindlem  50493