Theorem unssd 4143

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

Syntax hints:   → wi 4   ∧ wa 395   ∪ cun 3897   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3440  df-un 3904  df-ss 3916

This theorem is referenced by:  uneqdifeq  4444  tpssi  4791  sofld  6142  unima  6906  fr3nr  7714  ordsuci  7750  resf1extb  7873  resf1ext2b  7874  xpord2pred  8084  xpord3pred  8091  frrlem13  8237  naddcllem  8600  ralxpmap  8829  marypha1lem  9327  wemapso2lem  9448  unwf  9713  rankunb  9753  ackbij1lem6  10125  ackbij1lem16  10135  ssfin4  10211  isfin1-3  10287  ttukeylem7  10416  fpwwe2lem12  10543  wuncval2  10648  inar1  10676  un0addcl  12424  un0mulcl  12425  ssfzunsnext  13479  fzosplit  13602  fzouzsplit  13604  hashf1lem1  14372  ccatrn  14507  trclfvlb3  14928  trclun  14931  relexpfld  14966  saddisj  16386  lcmfunsnlem2lem1  16559  lcmfunsnlem2lem2  16560  lcmfunsnlem2  16561  lcmfun  16566  prmreclem5  16842  4sqlem11  16877  4sqlem19  16885  vdwlem1  16903  vdwlem12  16914  ramub1lem1  16948  ramub1lem2  16949  mrieqvlemd  17545  mreexmrid  17559  mreexexlem2d  17561  mreexexlem3d  17562  mreexexlem4d  17563  acsfiindd  18469  tsrdir  18520  f1omvdco2  19370  symgsssg  19389  symggen  19392  lsmunss  19581  efgsfo  19661  lsptpcl  20922  lspun  20930  lsmsp  21030  lspsolvlem  21089  lspsolv  21090  lsppratlem3  21096  lsppratlem4  21097  islbs3  21102  lbsextlem4  21108  aspval2  21845  evlseu  22028  mhpaddcl  22076  clslp  23073  neitr  23105  ordtuni  23115  ordtbas2  23116  ordtbas  23117  ordtrest  23127  cmpcld  23327  comppfsc  23457  1stckgenlem  23478  1stckgen  23479  ptbasfi  23506  fbun  23765  trfil2  23812  isufil2  23833  ufileu  23844  filufint  23845  fmfnfm  23883  hausflim  23906  flimclslem  23909  fclsfnflim  23952  flimfnfcls  23953  alexsubALTlem3  23974  alexsubALTlem4  23975  tsmsgsum  24064  tsmsres  24069  tsmsxplem1  24078  ustund  24147  trust  24154  ustuqtop1  24166  prdsdsf  24292  prdsxmetlem  24293  prdsmet  24295  prdsbl  24416  prdsxmslem2  24454  restmetu  24495  icccmplem2  24749  rrxmval  25342  rrxmet  25345  rrxdstprj1  25346  ovolunlem1  25435  ovolunnul  25438  nulmbl2  25474  volun  25483  volcn  25544  itgsplitioo  25776  limcvallem  25809  limcdif  25814  ellimc2  25815  limcres  25824  limccnp  25829  limccnp2  25830  limcco  25831  dvreslem  25847  dvres2lem  25848  dvaddbr  25877  dvmulbr  25878  dvmulbrOLD  25879  lhop2  25957  dvcnvrelem2  25960  elply2  26138  plyf  26140  elplyr  26143  elplyd  26144  ply1term  26146  ply0  26150  plyeq0lem  26152  plyeq0  26153  plyaddlem  26157  plymullem  26158  dgrlem  26171  coeidlem  26179  plyco  26183  plycj  26220  plycjOLD  26222  aannenlem2  26274  xrlimcnp  26915  perfectlem2  27178  noextend  27615  ssltun1  27759  ssltun2  27760  cutlt  27886  lrrecpred  27897  addsproplem2  27923  addsuniflem  27954  addsbday  27970  negsid  27993  mulsproplem9  28073  ssltmul1  28096  ssltmul2  28097  precsexlem8  28162  precsexlem11  28165  onaddscl  28220  shlej1  31351  shlub  31405  disjiunel  32587  fcoinver  32595  gsumzresunsn  33047  gsumwun  33056  elrgspnsubrunlem1  33225  elrgspnsubrunlem2  33226  elrgspnsubrun  33227  lsmidl  33377  elrspunsn  33405  mxidlprm  33446  qsdrngilem  33470  lindsun  33649  fldgenfldext  33692  evls1fldgencl  33694  fldextrspunlem1  33699  fldextrspunfld  33700  fldextrspunlem2  33701  fldextrspundgdvdslem  33704  fldextrspundgdvds  33705  algextdeglem1  33741  algextdeglem2  33742  algextdeglem3  33743  algextdeglem4  33744  algextdeglem5  33745  rtelextdg2  33751  constrextdg2lem  33772  constrext2chnlem  33774  constrfiss  33775  constrllcllem  33776  constrlccllem  33777  constrcccllem  33778  ordtrestNEW  33945  carsggect  34342  eulerpartlemt  34395  hgt750lemb  34680  hgt750leme  34682  bnj1136  35020  bnj1452  35075  erdszelem8  35253  mclsssvlem  35617  mclsax  35624  mclsind  35625  mthmpps  35637  mclsppslem  35638  topjoin  36420  weiunse  36523  poimirlem32  37702  ftc1anclem7  37749  ftc1anc  37751  prdsbnd  37843  rrnequiv  37885  pclfinN  40009  dochdmj1  41499  djhspss  41515  djhunssN  41518  djhlsmcl  41523  dvh4dimlem  41552  dvhdimlem  41553  lclkrlem2c  41618  lclkrlem2v  41637  mapdh9a  41898  hdmapval0  41942  hdmapval3lemN  41946  hdmap10lem  41948  deg1gprod  42243  dvun  42467  elrfi  42801  cmpfiiin  42804  istopclsd  42807  mzpcompact2lem  42858  eldioph2lem2  42868  eldioph2  42869  rngunsnply  43276  idomsubgmo  43300  omabs2  43439  dfrcl2  43781  iunrelexp0  43809  relexp0a  43823  brtrclfv2  43834  frege77d  43853  frege109d  43864  frege131d  43871  clsk3nimkb  44147  isotone1  44155  ntrclskb  44176  ntrclsk3  44177  ntrclsk13  44178  ntrneixb  44202  ntrneix3  44204  ntrneix13  44206  infxrpnf  45558  pimxrneun  45600  mccllem  45711  limciccioolb  45735  limcicciooub  45749  limcresiooub  45754  limcresioolb  45755  icccncfext  45999  dvnprodlem2  46059  ovolsplit  46100  fourierdlem20  46239  fourierdlem46  46264  fourierdlem48  46266  fourierdlem49  46267  fourierdlem50  46268  fourierdlem51  46269  fourierdlem54  46272  fourierdlem64  46282  fourierdlem76  46294  fourierdlem101  46319  fourierdlem102  46320  fourierdlem103  46321  fourierdlem104  46322  fourierdlem114  46332  sge0resplit  46518  sge0xaddlem1  46545  ismeannd  46579  caragenuncl  46625  omeunle  46628  isomenndlem  46642  hoidmvlelem2  46708  hoidmvlelem3  46709  hoidmvlelem4  46710  perfectALTVlem2  47836  gpgprismgriedgdmss  48166  pgindlem  49830