Theorem unssd 4138

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∪ cun 3897   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916

This theorem is used by:  uneqdifeq  4448  tpssi  4798  sofld  6179  unima  6960  fr3nr  7786  ordsuci  7822  resf1extb  7946  resf1ext2b  7947  xpord2pred  8162  xpord3pred  8169  frrlem13  8316  naddcllem  8685  ralxpmap  8924  marypha1lem  9425  wemapso2lem  9546  unwf  9818  rankunb  9864  ackbij1lem6  10302  ackbij1lem16  10312  ssfin4  10388  isfin1-3  10464  ttukeylem7  10593  fpwwe2lem12  10727  wuncval2  10832  inar1  10860  un0addcl  12639  un0mulcl  12640  ssfzunsnext  13703  fzosplit  13827  fzouzsplit  13829  hashf1lem1  14600  ccatrn  14735  trclfvlb3  15164  trclun  15167  relexpfld  15202  saddisj  16635  lcmfunsnlem2lem1  16813  lcmfunsnlem2lem2  16814  lcmfunsnlem2  16815  lcmfun  16820  prmreclem5  17098  4sqlem11  17133  4sqlem19  17141  vdwlem1  17159  vdwlem12  17170  ramub1lem1  17204  ramub1lem2  17205  mrieqvlemd  17803  mreexmrid  17817  mreexexlem2d  17819  mreexexlem3d  17820  mreexexlem4d  17821  acsfiindd  18727  tsrdir  18778  f1omvdco2  19662  symgsssg  19681  symggen  19684  lsmunss  19873  efgsfo  19953  lsptpcl  21254  lspun  21262  lsmsp  21361  lspsolvlem  21420  lspsolv  21421  lsppratlem3  21427  lsppratlem4  21428  islbs3  21433  lbsextlem4  21439  lsmidl  21538  aspval2  22206  evlseu  22392  mhpaddcl  22472  clslp  23466  neitr  23498  ordtuni  23508  ordtbas2  23509  ordtbas  23510  ordtrest  23520  cmpcld  23720  comppfsc  23851  1stckgenlem  23872  1stckgen  23873  ptbasfi  23900  fbun  24159  trfil2  24206  isufil2  24227  ufileu  24238  filufint  24239  fmfnfm  24277  hausflim  24300  flimclslem  24303  fclsfnflim  24346  flimfnfcls  24347  alexsubALTlem3  24368  alexsubALTlem4  24369  tsmsgsum  24458  tsmsres  24463  tsmsxplem1  24472  ustund  24541  trust  24548  ustuqtop1  24560  prdsdsf  24686  prdsxmetlem  24687  prdsmet  24689  prdsbl  24810  prdsxmslem2  24848  restmetu  24889  icccmplem2  25143  rrxmval  25726  rrxmet  25729  rrxdstprj1  25730  ovolunlem1  25818  ovolunnul  25821  nulmbl2  25857  volun  25866  volcn  25927  itgsplitioo  26158  limcvallem  26191  limcdif  26196  ellimc2  26197  limcres  26206  limccnp  26211  limccnp2  26212  limcco  26213  dvreslem  26229  dvres2lem  26230  dvaddbr  26258  dvmulbr  26259  lhop2  26335  dvcnvrelem2  26338  elply2  26514  plyf  26516  elplyr  26519  elplyd  26520  ply1term  26522  ply0  26526  plyeq0lem  26529  plyeq0  26530  plyaddlem  26534  plymullem  26535  dgrlem  26548  coeidlem  26556  plyco  26560  plycj  26596  aannenlem2  26656  xrlimcnp  27296  perfectlem2  27557  noextend  28023  sltsun1  28174  sltsun2  28175  cutlt  28318  lrrecpred  28330  addsproplem2  28356  addsuniflem  28387  addbday  28404  negsid  28427  mulsproplem9  28510  sltmuls1  28533  sltmuls2  28534  precsexlem8  28600  precsexlem11  28603  onaddscl  28663  bdaypw2n0bndlem  28849  shlej1  31962  shlub  32016  disjiunel  33190  fcoinver  33198  gsumzresunsn  33623  gsumwun  33637  elrgspnsubrunlem1  33808  elrgspnsubrunlem2  33809  elrgspnsubrun  33810  elrspunsn  33979  mxidlprm  33995  qsdrngilem  34018  esplyind  34207  lindsun  34257  fldgenfldext  34300  evls1fldgencl  34302  fldextrspunlem1  34307  fldextrspunfld  34308  fldextrspunlem2  34309  fldextrspundgdvdslem  34312  fldextrspundgdvds  34313  algextdeglem1  34349  algextdeglem2  34350  algextdeglem3  34351  algextdeglem4  34352  algextdeglem5  34353  rtelextdg2  34359  constrextdg2lem  34380  constrext2chnlem  34382  constrfiss  34383  constrllcllem  34384  constrlccllem  34385  constrcccllem  34386  ordtrestNEW  34553  carsggect  34950  eulerpartlemt  35003  hgt750lemb  35285  hgt750leme  35287  bnj1136  35627  bnj1452  35682  erdszelem8  35963  mclsssvlem  36327  mclsax  36334  mclsind  36335  mthmpps  36347  mclsppslem  36348  topjoin  37153  weiunse  37256  poimirlem32  38570  ftc1anclem7  38617  ftc1anc  38619  prdsbnd  38727  rrnequiv  38769  pclfinN  40957  dochdmj1  42447  djhspss  42463  djhunssN  42466  djhlsmcl  42471  dvh4dimlem  42500  dvhdimlem  42501  lclkrlem2c  42566  lclkrlem2v  42585  mapdh9a  42846  hdmapval0  42890  hdmapval3lemN  42894  hdmap10lem  42896  deg1gprod  43190  dvun  43410  elrfi  43704  cmpfiiin  43707  istopclsd  43710  mzpcompact2lem  43761  eldioph2lem2  43771  eldioph2  43772  rngunsnply  44170  idomsubgmo  44194  omabs2  44333  dfrcl2  44673  iunrelexp0  44701  relexp0a  44715  brtrclfv2  44726  frege77d  44745  frege109d  44756  frege131d  44763  clsk3nimkb  45039  isotone1  45047  ntrclskb  45068  ntrclsk3  45069  ntrclsk13  45070  ntrneixb  45094  ntrneix3  45096  ntrneix13  45098  infxrpnf  46455  pimxrneun  46497  mccllem  46608  limciccioolb  46632  limcicciooub  46646  limcresiooub  46651  limcresioolb  46652  icccncfext  46896  dvnprodlem2  46956  ovolsplit  46997  fourierdlem20  47136  fourierdlem46  47161  fourierdlem48  47163  fourierdlem49  47164  fourierdlem50  47165  fourierdlem51  47166  fourierdlem54  47169  fourierdlem64  47179  fourierdlem76  47191  fourierdlem101  47216  fourierdlem102  47217  fourierdlem103  47218  fourierdlem104  47219  fourierdlem114  47229  sge0resplit  47415  sge0xaddlem1  47442  ismeannd  47476  caragenuncl  47522  omeunle  47525  isomenndlem  47539  hoidmvlelem2  47605  hoidmvlelem3  47606  hoidmvlelem4  47607  perfectALTVlem2  48819  gpgprismgriedgdmss  49149  pgindlem  50807