Theorem unssd 4151

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

Syntax hints:   → wi 4   ∧ wa 396   ∪ cun 3911   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-un 3918  df-in 3920  df-ss 3930

This theorem is referenced by:  uneqdifeq  4455  tpssi  4801  sofld  6144  unima  6921  fr3nr  7711  ordsuci  7748  sucexeloniOLD  7750  suceloniOLD  7752  xpord2pred  8082  xpord3pred  8089  frrlem13  8234  naddcllem  8627  ralxpmap  8841  marypha1lem  9378  wemapso2lem  9497  unwf  9755  rankunb  9795  ackbij1lem6  10170  ackbij1lem16  10180  ssfin4  10255  isfin1-3  10331  ttukeylem7  10460  fpwwe2lem12  10587  wuncval2  10692  inar1  10720  un0addcl  12455  un0mulcl  12456  ssfzunsnext  13496  fzosplit  13615  fzouzsplit  13617  hashf1lem1  14365  hashf1lem1OLD  14366  ccatrn  14489  trclfvlb3  14908  trclun  14911  relexpfld  14946  saddisj  16356  lcmfunsnlem2lem1  16525  lcmfunsnlem2lem2  16526  lcmfunsnlem2  16527  lcmfun  16532  prmreclem5  16803  4sqlem11  16838  4sqlem19  16846  vdwlem1  16864  vdwlem12  16875  ramub1lem1  16909  ramub1lem2  16910  mrieqvlemd  17523  mreexmrid  17537  mreexexlem2d  17539  mreexexlem3d  17540  mreexexlem4d  17541  acsfiindd  18456  tsrdir  18507  f1omvdco2  19244  symgsssg  19263  symggen  19266  lsmunss  19455  efgsfo  19535  lsptpcl  20497  lspun  20505  lsmsp  20604  lspsolvlem  20662  lspsolv  20663  lsppratlem3  20669  lsppratlem4  20670  islbs3  20675  lbsextlem4  20681  aspval2  21338  evlseu  21530  mhpaddcl  21578  clslp  22536  neitr  22568  ordtuni  22578  ordtbas2  22579  ordtbas  22580  ordtrest  22590  cmpcld  22790  comppfsc  22920  1stckgenlem  22941  1stckgen  22942  ptbasfi  22969  fbun  23228  trfil2  23275  isufil2  23296  ufileu  23307  filufint  23308  fmfnfm  23346  hausflim  23369  flimclslem  23372  fclsfnflim  23415  flimfnfcls  23416  alexsubALTlem3  23437  alexsubALTlem4  23438  tsmsgsum  23527  tsmsres  23532  tsmsxplem1  23541  ustund  23610  trust  23618  ustuqtop1  23630  prdsdsf  23757  prdsxmetlem  23758  prdsmet  23760  prdsbl  23884  prdsxmslem2  23922  restmetu  23963  icccmplem2  24223  rrxmval  24806  rrxmet  24809  rrxdstprj1  24810  ovolunlem1  24898  ovolunnul  24901  nulmbl2  24937  volun  24946  volcn  25007  itgsplitioo  25239  limcvallem  25272  limcdif  25277  ellimc2  25278  limcres  25287  limccnp  25292  limccnp2  25293  limcco  25294  dvreslem  25310  dvres2lem  25311  dvaddbr  25339  dvmulbr  25340  lhop2  25416  dvcnvrelem2  25419  elply2  25594  plyf  25596  elplyr  25599  elplyd  25600  ply1term  25602  ply0  25606  plyeq0lem  25608  plyeq0  25609  plyaddlem  25613  plymullem  25614  dgrlem  25627  coeidlem  25635  plyco  25639  plycj  25675  aannenlem2  25726  xrlimcnp  26355  perfectlem2  26615  noextend  27051  ssltun1  27190  ssltun2  27191  lrrecpred  27299  addsproplem2  27325  addsunif  27353  negsid  27382  mulsproplem10  27431  shlej1  30365  shlub  30419  disjiunel  31581  fcoinver  31592  gsumzresunsn  31966  lsmidl  32255  mxidlprm  32313  lindsun  32407  ordtrestNEW  32591  carsggect  33007  eulerpartlemt  33060  hgt750lemb  33358  hgt750leme  33360  bnj1136  33698  bnj1452  33753  erdszelem8  33879  mclsssvlem  34243  mclsax  34250  mclsind  34251  mthmpps  34263  mclsppslem  34264  topjoin  34913  poimirlem32  36183  ftc1anclem7  36230  ftc1anc  36232  prdsbnd  36325  rrnequiv  36367  pclfinN  38436  dochdmj1  39926  djhspss  39942  djhunssN  39945  djhlsmcl  39950  dvh4dimlem  39979  dvhdimlem  39980  lclkrlem2c  40045  lclkrlem2v  40064  mapdh9a  40325  hdmapval0  40369  hdmapval3lemN  40373  hdmap10lem  40375  elrfi  41075  cmpfiiin  41078  istopclsd  41081  mzpcompact2lem  41132  eldioph2lem2  41142  eldioph2  41143  rngunsnply  41558  idomsubgmo  41583  omabs2  41725  dfrcl2  42068  iunrelexp0  42096  relexp0a  42110  brtrclfv2  42121  frege77d  42140  frege109d  42151  frege131d  42158  clsk3nimkb  42434  isotone1  42442  ntrclskb  42463  ntrclsk3  42464  ntrclsk13  42465  ntrneixb  42489  ntrneix3  42491  ntrneix13  42493  infxrpnf  43801  pimxrneun  43844  mccllem  43958  limciccioolb  43982  limcicciooub  43998  limcresiooub  44003  limcresioolb  44004  icccncfext  44248  dvnprodlem2  44308  ovolsplit  44349  fourierdlem20  44488  fourierdlem46  44513  fourierdlem48  44515  fourierdlem49  44516  fourierdlem50  44517  fourierdlem51  44518  fourierdlem54  44521  fourierdlem64  44531  fourierdlem76  44543  fourierdlem101  44568  fourierdlem102  44569  fourierdlem103  44570  fourierdlem104  44571  fourierdlem114  44581  sge0resplit  44767  sge0xaddlem1  44794  ismeannd  44828  caragenuncl  44874  omeunle  44877  isomenndlem  44891  hoidmvlelem2  44957  hoidmvlelem3  44958  hoidmvlelem4  44959  perfectALTVlem2  46034  pgindlem  47280