Theorem unssd 4100

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

Syntax hints:   → wi 4   ∧ wa 399   ∪ cun 3864   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-un 3871  df-in 3873  df-ss 3883

This theorem is referenced by:  uneqdifeq  4404  tpssi  4749  sofld  6050  unima  6786  fr3nr  7557  suceloni  7592  frrlem13  8039  ralxpmap  8577  marypha1lem  9049  wemapso2lem  9168  dftrpred3g  9339  unwf  9426  rankunb  9466  ackbij1lem6  9839  ackbij1lem16  9849  ssfin4  9924  isfin1-3  10000  ttukeylem7  10129  fpwwe2lem12  10256  wuncval2  10361  inar1  10389  un0addcl  12123  un0mulcl  12124  ssfzunsnext  13157  fzosplit  13275  fzouzsplit  13277  hashf1lem1  14020  hashf1lem1OLD  14021  ccatrn  14146  trclfvlb3  14574  trclun  14577  relexpfld  14612  saddisj  16024  lcmfunsnlem2lem1  16195  lcmfunsnlem2lem2  16196  lcmfunsnlem2  16197  lcmfun  16202  prmreclem5  16473  4sqlem11  16508  4sqlem19  16516  vdwlem1  16534  vdwlem12  16545  ramub1lem1  16579  ramub1lem2  16580  mrieqvlemd  17132  mreexmrid  17146  mreexexlem2d  17148  mreexexlem3d  17149  mreexexlem4d  17150  acsfiindd  18059  tsrdir  18110  f1omvdco2  18840  symgsssg  18859  symggen  18862  lsmunss  19048  efgsfo  19129  lsptpcl  20016  lspun  20024  lsmsp  20123  lspsolvlem  20179  lspsolv  20180  lsppratlem3  20186  lsppratlem4  20187  islbs3  20192  lbsextlem4  20198  aspval2  20858  evlseu  21043  mhpaddcl  21091  clslp  22045  neitr  22077  ordtuni  22087  ordtbas2  22088  ordtbas  22089  ordtrest  22099  cmpcld  22299  comppfsc  22429  1stckgenlem  22450  1stckgen  22451  ptbasfi  22478  fbun  22737  trfil2  22784  isufil2  22805  ufileu  22816  filufint  22817  fmfnfm  22855  hausflim  22878  flimclslem  22881  fclsfnflim  22924  flimfnfcls  22925  alexsubALTlem3  22946  alexsubALTlem4  22947  tsmsgsum  23036  tsmsres  23041  tsmsxplem1  23050  ustund  23119  trust  23127  ustuqtop1  23139  prdsdsf  23265  prdsxmetlem  23266  prdsmet  23268  prdsbl  23389  prdsxmslem2  23427  restmetu  23468  icccmplem2  23720  rrxmval  24302  rrxmet  24305  rrxdstprj1  24306  ovolunlem1  24394  ovolunnul  24397  nulmbl2  24433  volun  24442  volcn  24503  itgsplitioo  24735  limcvallem  24768  limcdif  24773  ellimc2  24774  limcres  24783  limccnp  24788  limccnp2  24789  limcco  24790  dvreslem  24806  dvres2lem  24807  dvaddbr  24835  dvmulbr  24836  lhop2  24912  dvcnvrelem2  24915  elply2  25090  plyf  25092  elplyr  25095  elplyd  25096  ply1term  25098  ply0  25102  plyeq0lem  25104  plyeq0  25105  plyaddlem  25109  plymullem  25110  dgrlem  25123  coeidlem  25131  plyco  25135  plycj  25171  aannenlem2  25222  xrlimcnp  25851  perfectlem2  26111  shlej1  29441  shlub  29495  disjiunel  30654  fcoinver  30665  gsumzresunsn  31033  lsmidl  31303  mxidlprm  31354  lindsun  31420  ordtrestNEW  31585  carsggect  31997  eulerpartlemt  32050  hgt750lemb  32348  hgt750leme  32350  bnj1136  32690  bnj1452  32745  erdszelem8  32873  mclsssvlem  33237  mclsax  33244  mclsind  33245  mthmpps  33257  mclsppslem  33258  xpord2pred  33529  xpord3pred  33535  naddcllem  33568  noextend  33606  ssltun1  33739  ssltun2  33740  lrrecpred  33838  topjoin  34291  poimirlem32  35546  ftc1anclem7  35593  ftc1anc  35595  prdsbnd  35688  rrnequiv  35730  pclfinN  37651  dochdmj1  39141  djhspss  39157  djhunssN  39160  djhlsmcl  39165  dvh4dimlem  39194  dvhdimlem  39195  lclkrlem2c  39260  lclkrlem2v  39279  mapdh9a  39540  hdmapval0  39584  hdmapval3lemN  39588  hdmap10lem  39590  elrfi  40219  cmpfiiin  40222  istopclsd  40225  mzpcompact2lem  40276  eldioph2lem2  40286  eldioph2  40287  rngunsnply  40701  idomsubgmo  40726  dfrcl2  40959  iunrelexp0  40987  relexp0a  41001  brtrclfv2  41012  frege77d  41031  frege109d  41042  frege131d  41049  clsk3nimkb  41327  isotone1  41335  ntrclskb  41356  ntrclsk3  41357  ntrclsk13  41358  ntrneixb  41382  ntrneix3  41384  ntrneix13  41386  infxrpnf  42660  mccllem  42813  limciccioolb  42837  limcicciooub  42853  limcresiooub  42858  limcresioolb  42859  icccncfext  43103  dvnprodlem2  43163  ovolsplit  43204  fourierdlem20  43343  fourierdlem46  43368  fourierdlem48  43370  fourierdlem49  43371  fourierdlem50  43372  fourierdlem51  43373  fourierdlem54  43376  fourierdlem64  43386  fourierdlem76  43398  fourierdlem101  43423  fourierdlem102  43424  fourierdlem103  43425  fourierdlem104  43426  fourierdlem114  43436  sge0resplit  43619  sge0xaddlem1  43646  ismeannd  43680  caragenuncl  43726  omeunle  43729  isomenndlem  43743  hoidmvlelem2  43809  hoidmvlelem3  43810  hoidmvlelem4  43811  perfectALTVlem2  44847