Theorem unssd 4193

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154

This theorem is used by:  uneqdifeq  4451  tpssi  4798  sofld  6197  unima  6991  fr3nr  7818  ordsuci  7856  resf1extb  7980  resf1ext2b  7981  xpord2pred  8199  xpord3pred  8206  frrlem13  8354  naddcllem  8723  ralxpmap  8962  marypha1lem  9462  wemapso2lem  9583  unwf  9855  rankunb  9901  ackbij1lem6  10341  ackbij1lem16  10351  ssfin4  10427  isfin1-3  10503  ttukeylem7  10632  fpwwe2lem12  10766  wuncval2  10871  inar1  10899  un0addcl  12679  un0mulcl  12680  ssfzunsnext  13743  fzosplit  13867  fzouzsplit  13869  hashf1lem1  14641  ccatrn  14776  trclfvlb3  15207  trclun  15210  relexpfld  15245  saddisj  16679  lcmfunsnlem2lem1  16857  lcmfunsnlem2lem2  16858  lcmfunsnlem2  16859  lcmfun  16864  prmreclem5  17142  4sqlem11  17177  4sqlem19  17185  vdwlem1  17203  vdwlem12  17214  ramub1lem1  17248  ramub1lem2  17249  mrieqvlemd  17853  mreexmrid  17867  mreexexlem2d  17869  mreexexlem3d  17870  mreexexlem4d  17871  acsfiindd  18777  tsrdir  18828  f1omvdco2  19713  symgsssg  19732  symggen  19735  lsmunss  19924  efgsfo  20004  lsptpcl  21305  lspun  21313  lsmsp  21412  lspsolvlem  21471  lspsolv  21472  lsppratlem3  21478  lsppratlem4  21479  islbs3  21484  lbsextlem4  21490  lsmidl  21589  aspval2  22261  evlseu  22447  mhpaddcl  22527  clslp  23521  neitr  23553  ordtuni  23563  ordtbas2  23564  ordtbas  23565  ordtrest  23575  cmpcld  23775  comppfsc  23906  1stckgenlem  23927  1stckgen  23928  ptbasfi  23955  fbun  24214  trfil2  24261  isufil2  24282  ufileu  24293  filufint  24294  fmfnfm  24332  hausflim  24355  flimclslem  24358  fclsfnflim  24401  flimfnfcls  24402  alexsubALTlem3  24423  alexsubALTlem4  24424  tsmsgsum  24513  tsmsres  24518  tsmsxplem1  24527  ustund  24596  trust  24603  ustuqtop1  24615  prdsdsf  24741  prdsxmetlem  24742  prdsmet  24744  prdsbl  24865  prdsxmslem2  24903  restmetu  24944  icccmplem2  25198  rrxmval  25781  rrxmet  25784  rrxdstprj1  25785  ovolunlem1  25873  ovolunnul  25876  nulmbl2  25912  volun  25921  volcn  25982  itgsplitioo  26213  limcvallem  26246  limcdif  26251  ellimc2  26252  limcres  26261  limccnp  26266  limccnp2  26267  limcco  26268  dvreslem  26284  dvres2lem  26285  dvaddbr  26313  dvmulbr  26314  lhop2  26390  dvcnvrelem2  26393  elply2  26569  plyf  26571  elplyr  26574  elplyd  26575  ply1term  26577  ply0  26581  plyeq0lem  26584  plyeq0  26585  plyaddlem  26589  plymullem  26590  dgrlem  26603  coeidlem  26611  plyco  26615  plycj  26651  rngunsnply  26693  aannenlem2  26713  xrlimcnp  27353  perfectlem2  27614  noextend  28080  sltsun1  28231  sltsun2  28232  cutlt  28375  lrrecpred  28387  addsproplem2  28413  addsuniflem  28444  addbday  28461  negsid  28484  mulsproplem9  28567  sltmuls1  28590  sltmuls2  28591  precsexlem8  28657  precsexlem11  28660  onaddscl  28720  bdaypw2n0bndlem  28906  shlej1  32019  shlub  32073  disjiunel  33288  fcoinver  33296  gsumzresunsn  33722  gsumwun  33736  elrgspnsubrunlem1  33907  elrgspnsubrunlem2  33908  elrgspnsubrun  33909  elrspunsn  34083  mxidlprm  34099  qsdrngilem  34122  evls1rgspncl  34248  rngunsnply1  34249  esplyind  34318  lindsun  34368  fldgenfldext  34411  evls1fldgencl  34413  fldextrspunlem1  34418  fldextrspunfld  34419  fldextrspunlem2  34420  fldextrspundgdvdslem  34423  fldextrspundgdvds  34424  algextdeglem1  34460  algextdeglem2  34461  algextdeglem3  34462  algextdeglem4  34463  algextdeglem5  34464  rtelextdg2  34470  constrextdg2lem  34491  constrext2chnlem  34493  constrfiss  34494  constrllcllem  34495  constrlccllem  34496  constrcccllem  34497  ordtrestNEW  34664  carsggect  35061  eulerpartlemt  35114  hgt750lemb  35396  hgt750leme  35398  bnj1136  35738  bnj1452  35793  erdszelem8  36171  mclsssvlem  36535  mclsax  36542  mclsind  36543  mthmpps  36555  mclsppslem  36556  topjoin  37368  weiunse  37471  poimirlem32  38838  ftc1anclem7  38885  ftc1anc  38887  prdsbnd  38993  rrnequiv  39035  pclfinN  41223  dochdmj1  42713  djhspss  42729  djhunssN  42732  djhlsmcl  42737  dvh4dimlem  42766  dvhdimlem  42767  lclkrlem2c  42832  lclkrlem2v  42851  mapdh9a  43112  hdmapval0  43156  hdmapval3lemN  43160  hdmap10lem  43162  deg1gprod  43456  dvun  43676  elrfi  43971  cmpfiiin  43974  istopclsd  43977  mzpcompact2lem  44028  eldioph2lem2  44038  eldioph2  44039  idomsubgmo  44456  omabs2  44595  dfrcl2  44935  iunrelexp0  44963  relexp0a  44977  brtrclfv2  44988  frege77d  45007  frege109d  45018  frege131d  45025  clsk3nimkb  45301  isotone1  45309  ntrclskb  45330  ntrclsk3  45331  ntrclsk13  45332  ntrneixb  45356  ntrneix3  45358  ntrneix13  45360  infxrpnf  46729  pimxrneun  46771  mccllem  46882  limciccioolb  46906  limcicciooub  46920  limcresiooub  46925  limcresioolb  46926  icccncfext  47170  dvnprodlem2  47230  ovolsplit  47271  fourierdlem20  47410  fourierdlem46  47435  fourierdlem48  47437  fourierdlem49  47438  fourierdlem50  47439  fourierdlem51  47440  fourierdlem54  47443  fourierdlem64  47453  fourierdlem76  47465  fourierdlem101  47490  fourierdlem102  47491  fourierdlem103  47492  fourierdlem104  47493  fourierdlem114  47503  sge0resplit  47689  sge0xaddlem1  47716  ismeannd  47750  caragenuncl  47796  omeunle  47799  isomenndlem  47813  hoidmvlelem2  47879  hoidmvlelem3  47880  hoidmvlelem4  47881  perfectALTVlem2  49093  gpgprismgriedgdmss  49423  azssid  49718  azcn  49720  pgindlem  51214