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

Theorem unssd 3772
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 3770 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
43biimpi 206 . 2 ((𝐴𝐶𝐵𝐶) → (𝐴𝐵) ⊆ 𝐶)
51, 2, 4syl2anc 692 1 (𝜑 → (𝐴𝐵) ⊆ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  cun 3558  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-v 3193  df-un 3565  df-in 3567  df-ss 3574
This theorem is referenced by:  uneqdifeq  4034  tpssi  4342  sofld  5544  fr3nr  6927  suceloni  6961  ralxpmap  7852  marypha1lem  8284  wemapso2lem  8402  unwf  8618  rankunb  8658  ackbij1lem6  8992  ackbij1lem16  9002  ssfin4  9077  isfin1-3  9153  ttukeylem7  9282  fpwwe2lem13  9409  wuncval2  9514  inar1  9542  un0addcl  11271  un0mulcl  11272  ssfzunsnext  12325  fzosplit  12439  fzouzsplit  12441  hashf1lem1  13174  ccatrn  13306  trclfvlb3  13681  trclun  13684  relexpfld  13718  saddisj  15106  lcmfunsnlem2lem1  15270  lcmfunsnlem2lem2  15271  lcmfunsnlem2  15272  lcmfun  15277  prmreclem5  15543  4sqlem11  15578  4sqlem19  15586  vdwlem1  15604  vdwlem12  15615  ramub1lem1  15649  ramub1lem2  15650  mrieqvlemd  16205  mreexmrid  16219  mreexexlem2d  16221  mreexexlem3d  16222  mreexexlem4d  16223  acsfiindd  17093  tsrdir  17154  f1omvdco2  17784  symgsssg  17803  symggen  17806  lsmunss  17989  efgsfo  18068  lsptpcl  18893  lspun  18901  lsmsp  19000  lspsolvlem  19056  lspsolv  19057  lsppratlem3  19063  lsppratlem4  19064  islbs3  19069  lbsextlem4  19075  aspval2  19261  evlseu  19430  clslp  20857  neitr  20889  ordtuni  20899  ordtbas2  20900  ordtbas  20901  ordtrest  20911  cmpcld  21110  comppfsc  21240  1stckgenlem  21261  1stckgen  21262  ptbasfi  21289  fbun  21549  trfil2  21596  isufil2  21617  ufileu  21628  filufint  21629  fmfnfm  21667  hausflim  21690  flimclslem  21693  fclsfnflim  21736  flimfnfcls  21737  alexsubALTlem3  21758  alexsubALTlem4  21759  tsmsgsum  21847  tsmsres  21852  tsmsxplem1  21861  ustund  21930  trust  21938  ustuqtop1  21950  prdsdsf  22077  prdsxmetlem  22078  prdsmet  22080  prdsbl  22201  prdsxmslem2  22239  restmetu  22280  icccmplem2  22529  rrxmval  23091  rrxmet  23094  rrxdstprj1  23095  ovolunlem1  23167  ovolunnul  23170  nulmbl2  23206  volun  23215  volcn  23275  itgsplitioo  23505  limcvallem  23536  limcdif  23541  ellimc2  23542  limcres  23551  limccnp  23556  limccnp2  23557  limcco  23558  dvreslem  23574  dvres2lem  23575  dvaddbr  23602  dvmulbr  23603  lhop2  23677  dvcnvrelem2  23680  elply2  23851  plyf  23853  elplyr  23856  elplyd  23857  ply1term  23859  ply0  23863  plyeq0lem  23865  plyeq0  23866  plyaddlem  23870  plymullem  23871  dgrlem  23884  coeidlem  23892  plyco  23896  plycj  23932  aannenlem2  23983  xrlimcnp  24590  perfectlem2  24850  shlej1  28059  shlub  28113  disjiunel  29245  fcoinver  29252  ordtrestNEW  29741  carsggect  30153  eulerpartlemt  30206  bnj1136  30765  bnj1452  30820  erdszelem8  30880  mclsssvlem  31159  mclsax  31166  mclsind  31167  mthmpps  31179  mclsppslem  31180  dftrpred3g  31426  noextend  31516  topjoin  31994  poimirlem32  33059  ftc1anclem7  33109  ftc1anc  33111  prdsbnd  33210  rrnequiv  33252  pclfinN  34652  dochdmj1  36145  djhspss  36161  djhunssN  36164  djhlsmcl  36169  dvh4dimlem  36198  dvhdimlem  36199  lclkrlem2c  36264  lclkrlem2v  36283  mapdh9a  36545  hdmapval0  36591  hdmapval3lemN  36595  hdmap10lem  36597  elrfi  36723  cmpfiiin  36726  istopclsd  36729  mzpcompact2lem  36780  eldioph2lem2  36790  eldioph2  36791  rngunsnply  37210  idomsubgmo  37243  dfrcl2  37433  iunrelexp0  37461  relexp0a  37475  brtrclfv2  37486  frege77d  37505  frege109d  37516  frege131d  37523  clsk3nimkb  37806  isotone1  37814  ntrclskb  37835  ntrclsk3  37836  ntrclsk13  37837  ntrneixb  37861  ntrneix3  37863  ntrneix13  37865  unima  38805  mccllem  39220  limciccioolb  39244  limcicciooub  39260  limcresiooub  39265  limcresioolb  39266  icccncfext  39391  dvnprodlem2  39455  ovolsplit  39499  fourierdlem20  39638  fourierdlem46  39663  fourierdlem48  39665  fourierdlem49  39666  fourierdlem50  39667  fourierdlem51  39668  fourierdlem54  39671  fourierdlem64  39681  fourierdlem76  39693  fourierdlem101  39718  fourierdlem102  39719  fourierdlem103  39720  fourierdlem104  39721  fourierdlem114  39731  sge0resplit  39917  sge0xaddlem1  39944  ismeannd  39978  caragenuncl  40021  omeunle  40024  isomenndlem  40038  hoidmvlelem2  40104  hoidmvlelem3  40105  hoidmvlelem4  40106  perfectALTVlem2  40914
  Copyright terms: Public domain W3C validator