MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unssd Structured version   Visualization version   GIF version

Theorem unssd 3822
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
StepHypRef Expression
1 unssd.1 . 2 (𝜑𝐴𝐶)
2 unssd.2 . 2 (𝜑𝐵𝐶)
3 unss 3820 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
43biimpi 206 . 2 ((𝐴𝐶𝐵𝐶) → (𝐴𝐵) ⊆ 𝐶)
51, 2, 4syl2anc 694 1 (𝜑 → (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  cun 3605  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-in 3614  df-ss 3621
This theorem is referenced by:  uneqdifeq  4090  tpssi  4401  sofld  5616  fr3nr  7021  suceloni  7055  ralxpmap  7949  marypha1lem  8380  wemapso2lem  8498  unwf  8711  rankunb  8751  ackbij1lem6  9085  ackbij1lem16  9095  ssfin4  9170  isfin1-3  9246  ttukeylem7  9375  fpwwe2lem13  9502  wuncval2  9607  inar1  9635  un0addcl  11364  un0mulcl  11365  ssfzunsnext  12424  fzosplit  12540  fzouzsplit  12542  hashf1lem1  13277  ccatrn  13407  trclfvlb3  13796  trclun  13799  relexpfld  13833  saddisj  15234  lcmfunsnlem2lem1  15398  lcmfunsnlem2lem2  15399  lcmfunsnlem2  15400  lcmfun  15405  prmreclem5  15671  4sqlem11  15706  4sqlem19  15714  vdwlem1  15732  vdwlem12  15743  ramub1lem1  15777  ramub1lem2  15778  mrieqvlemd  16336  mreexmrid  16350  mreexexlem2d  16352  mreexexlem3d  16353  mreexexlem4d  16354  acsfiindd  17224  tsrdir  17285  f1omvdco2  17914  symgsssg  17933  symggen  17936  lsmunss  18119  efgsfo  18198  lsptpcl  19027  lspun  19035  lsmsp  19134  lspsolvlem  19190  lspsolv  19191  lsppratlem3  19197  lsppratlem4  19198  islbs3  19203  lbsextlem4  19209  aspval2  19395  evlseu  19564  clslp  21000  neitr  21032  ordtuni  21042  ordtbas2  21043  ordtbas  21044  ordtrest  21054  cmpcld  21253  comppfsc  21383  1stckgenlem  21404  1stckgen  21405  ptbasfi  21432  fbun  21691  trfil2  21738  isufil2  21759  ufileu  21770  filufint  21771  fmfnfm  21809  hausflim  21832  flimclslem  21835  fclsfnflim  21878  flimfnfcls  21879  alexsubALTlem3  21900  alexsubALTlem4  21901  tsmsgsum  21989  tsmsres  21994  tsmsxplem1  22003  ustund  22072  trust  22080  ustuqtop1  22092  prdsdsf  22219  prdsxmetlem  22220  prdsmet  22222  prdsbl  22343  prdsxmslem2  22381  restmetu  22422  icccmplem2  22673  rrxmval  23234  rrxmet  23237  rrxdstprj1  23238  ovolunlem1  23311  ovolunnul  23314  nulmbl2  23350  volun  23359  volcn  23420  itgsplitioo  23649  limcvallem  23680  limcdif  23685  ellimc2  23686  limcres  23695  limccnp  23700  limccnp2  23701  limcco  23702  dvreslem  23718  dvres2lem  23719  dvaddbr  23746  dvmulbr  23747  lhop2  23823  dvcnvrelem2  23826  elply2  23997  plyf  23999  elplyr  24002  elplyd  24003  ply1term  24005  ply0  24009  plyeq0lem  24011  plyeq0  24012  plyaddlem  24016  plymullem  24017  dgrlem  24030  coeidlem  24038  plyco  24042  plycj  24078  aannenlem2  24129  xrlimcnp  24740  perfectlem2  25000  shlej1  28347  shlub  28401  disjiunel  29535  fcoinver  29544  ordtrestNEW  30095  carsggect  30508  eulerpartlemt  30561  hgt750lemb  30862  hgt750leme  30864  bnj1136  31191  bnj1452  31246  erdszelem8  31306  mclsssvlem  31585  mclsax  31592  mclsind  31593  mthmpps  31605  mclsppslem  31606  dftrpred3g  31857  noextend  31944  ssltun1  32040  ssltun2  32041  topjoin  32485  poimirlem32  33571  ftc1anclem7  33621  ftc1anc  33623  prdsbnd  33722  rrnequiv  33764  pclfinN  35504  dochdmj1  36996  djhspss  37012  djhunssN  37015  djhlsmcl  37020  dvh4dimlem  37049  dvhdimlem  37050  lclkrlem2c  37115  lclkrlem2v  37134  mapdh9a  37396  hdmapval0  37442  hdmapval3lemN  37446  hdmap10lem  37448  elrfi  37574  cmpfiiin  37577  istopclsd  37580  mzpcompact2lem  37631  eldioph2lem2  37641  eldioph2  37642  rngunsnply  38060  idomsubgmo  38093  dfrcl2  38283  iunrelexp0  38311  relexp0a  38325  brtrclfv2  38336  frege77d  38355  frege109d  38366  frege131d  38373  clsk3nimkb  38655  isotone1  38663  ntrclskb  38684  ntrclsk3  38685  ntrclsk13  38686  ntrneixb  38710  ntrneix3  38712  ntrneix13  38714  unima  39660  infxrpnf  39987  mccllem  40147  limciccioolb  40171  limcicciooub  40187  limcresiooub  40192  limcresioolb  40193  icccncfext  40418  dvnprodlem2  40480  ovolsplit  40523  fourierdlem20  40662  fourierdlem46  40687  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem51  40692  fourierdlem54  40695  fourierdlem64  40705  fourierdlem76  40717  fourierdlem101  40742  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem114  40755  sge0resplit  40941  sge0xaddlem1  40968  ismeannd  41002  caragenuncl  41048  omeunle  41051  isomenndlem  41065  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvlelem4  41133  perfectALTVlem2  41956
  Copyright terms: Public domain W3C validator