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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916

This theorem is used by:  uneqdifeq  4448  tpssi  4798  sofld  6180  unima  6954  fr3nr  7772  ordsuci  7808  resf1extb  7932  resf1ext2b  7933  xpord2pred  8144  xpord3pred  8151  frrlem13  8298  naddcllem  8665  ralxpmap  8904  marypha1lem  9404  wemapso2lem  9525  unwf  9793  rankunb  9833  ackbij1lem6  10227  ackbij1lem16  10237  ssfin4  10313  isfin1-3  10389  ttukeylem7  10518  fpwwe2lem12  10652  wuncval2  10757  inar1  10785  un0addcl  12562  un0mulcl  12563  ssfzunsnext  13625  fzosplit  13749  fzouzsplit  13751  hashf1lem1  14521  ccatrn  14656  trclfvlb3  15085  trclun  15088  relexpfld  15123  saddisj  16556  lcmfunsnlem2lem1  16729  lcmfunsnlem2lem2  16730  lcmfunsnlem2  16731  lcmfun  16736  prmreclem5  17013  4sqlem11  17048  4sqlem19  17056  vdwlem1  17074  vdwlem12  17085  ramub1lem1  17119  ramub1lem2  17120  mrieqvlemd  17718  mreexmrid  17732  mreexexlem2d  17734  mreexexlem3d  17735  mreexexlem4d  17736  acsfiindd  18642  tsrdir  18693  f1omvdco2  19576  symgsssg  19595  symggen  19598  lsmunss  19787  efgsfo  19867  lsptpcl  21164  lspun  21172  lsmsp  21271  lspsolvlem  21330  lspsolv  21331  lsppratlem3  21337  lsppratlem4  21338  islbs3  21343  lbsextlem4  21349  lsmidl  21448  aspval2  22114  evlseu  22300  mhpaddcl  22380  clslp  23374  neitr  23406  ordtuni  23416  ordtbas2  23417  ordtbas  23418  ordtrest  23428  cmpcld  23628  comppfsc  23759  1stckgenlem  23780  1stckgen  23781  ptbasfi  23808  fbun  24067  trfil2  24114  isufil2  24135  ufileu  24146  filufint  24147  fmfnfm  24185  hausflim  24208  flimclslem  24211  fclsfnflim  24254  flimfnfcls  24255  alexsubALTlem3  24276  alexsubALTlem4  24277  tsmsgsum  24366  tsmsres  24371  tsmsxplem1  24380  ustund  24449  trust  24456  ustuqtop1  24468  prdsdsf  24594  prdsxmetlem  24595  prdsmet  24597  prdsbl  24718  prdsxmslem2  24756  restmetu  24797  icccmplem2  25051  rrxmval  25634  rrxmet  25637  rrxdstprj1  25638  ovolunlem1  25726  ovolunnul  25729  nulmbl2  25765  volun  25774  volcn  25835  itgsplitioo  26066  limcvallem  26099  limcdif  26104  ellimc2  26105  limcres  26114  limccnp  26119  limccnp2  26120  limcco  26121  dvreslem  26137  dvres2lem  26138  dvaddbr  26166  dvmulbr  26167  lhop2  26243  dvcnvrelem2  26246  elply2  26422  plyf  26424  elplyr  26427  elplyd  26428  ply1term  26430  ply0  26434  plyeq0lem  26437  plyeq0  26438  plyaddlem  26442  plymullem  26443  dgrlem  26456  coeidlem  26464  plyco  26468  plycj  26504  plycjOLD  26506  aannenlem2  26566  xrlimcnp  27206  perfectlem2  27467  noextend  27903  sltsun1  28054  sltsun2  28055  cutlt  28198  lrrecpred  28210  addsproplem2  28236  addsuniflem  28267  addbday  28284  negsid  28307  mulsproplem9  28390  sltmuls1  28413  sltmuls2  28414  precsexlem8  28480  precsexlem11  28483  onaddscl  28543  bdaypw2n0bndlem  28729  shlej1  31842  shlub  31896  disjiunel  33070  fcoinver  33078  gsumzresunsn  33503  gsumwun  33517  elrgspnsubrunlem1  33688  elrgspnsubrunlem2  33689  elrgspnsubrun  33690  elrspunsn  33858  mxidlprm  33874  qsdrngilem  33897  esplyind  34086  lindsun  34136  fldgenfldext  34179  evls1fldgencl  34181  fldextrspunlem1  34186  fldextrspunfld  34187  fldextrspunlem2  34188  fldextrspundgdvdslem  34191  fldextrspundgdvds  34192  algextdeglem1  34228  algextdeglem2  34229  algextdeglem3  34230  algextdeglem4  34231  algextdeglem5  34232  rtelextdg2  34238  constrextdg2lem  34259  constrext2chnlem  34261  constrfiss  34262  constrllcllem  34263  constrlccllem  34264  constrcccllem  34265  ordtrestNEW  34432  carsggect  34830  eulerpartlemt  34883  hgt750lemb  35165  hgt750leme  35167  bnj1136  35507  bnj1452  35562  erdszelem8  35778  mclsssvlem  36142  mclsax  36149  mclsind  36150  mthmpps  36162  mclsppslem  36163  topjoin  36985  weiunse  37088  poimirlem32  38402  ftc1anclem7  38449  ftc1anc  38451  prdsbnd  38544  rrnequiv  38586  pclfinN  40774  dochdmj1  42264  djhspss  42280  djhunssN  42283  djhlsmcl  42288  dvh4dimlem  42317  dvhdimlem  42318  lclkrlem2c  42383  lclkrlem2v  42402  mapdh9a  42663  hdmapval0  42707  hdmapval3lemN  42711  hdmap10lem  42713  deg1gprod  43007  dvun  43235  elrfi  43540  cmpfiiin  43543  istopclsd  43546  mzpcompact2lem  43597  eldioph2lem2  43607  eldioph2  43608  rngunsnply  44011  idomsubgmo  44035  omabs2  44174  dfrcl2  44515  iunrelexp0  44543  relexp0a  44557  brtrclfv2  44568  frege77d  44587  frege109d  44598  frege131d  44605  clsk3nimkb  44881  isotone1  44889  ntrclskb  44910  ntrclsk3  44911  ntrclsk13  44912  ntrneixb  44936  ntrneix3  44938  ntrneix13  44940  infxrpnf  46275  pimxrneun  46317  mccllem  46428  limciccioolb  46452  limcicciooub  46466  limcresiooub  46471  limcresioolb  46472  icccncfext  46716  dvnprodlem2  46776  ovolsplit  46817  fourierdlem20  46956  fourierdlem46  46981  fourierdlem48  46983  fourierdlem49  46984  fourierdlem50  46985  fourierdlem51  46986  fourierdlem54  46989  fourierdlem64  46999  fourierdlem76  47011  fourierdlem101  47036  fourierdlem102  47037  fourierdlem103  47038  fourierdlem104  47039  fourierdlem114  47049  sge0resplit  47235  sge0xaddlem1  47262  ismeannd  47296  caragenuncl  47342  omeunle  47345  isomenndlem  47359  hoidmvlelem2  47425  hoidmvlelem3  47426  hoidmvlelem4  47427  perfectALTVlem2  48639  gpgprismgriedgdmss  48969  pgindlem  50642