MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfss2 Unicode version

Theorem dfss2 3492
Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of [TakeutiZaring] p. 17. (Contributed by NM, 8-Jan-2002.)
Assertion
Ref Expression
dfss2
Distinct variable groups:   ,   ,

Proof of Theorem dfss2
StepHypRef Expression
1 dfss 3490 . . 3
2 df-in 3482 . . . 4
32eqeq2i 2475 . . 3
4 abeq2 2581 . . 3
51, 3, 43bitri 271 . 2
6 pm4.71 630 . . 3
76albii 1640 . 2
85, 7bitr4i 252 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  e.wcel 1818  {cab 2442  i^icin 3474  C_wss 3475
This theorem is referenced by:  dfss3  3493  dfss2f  3494  ssel  3497  ssriv  3507  ssrdv  3509  sstr2  3510  eqss  3518  nss  3561  rabss2  3582  ssconb  3636  ssequn1  3673  unss  3677  ssin  3719  reldisj  3870  ssdif0  3885  difin0ss  3894  inssdif0  3895  ssundif  3911  sbcssg  3940  pwss  4027  snss  4154  pwpw0  4178  pwsnALT  4244  ssuni  4271  unissb  4281  intssOLD  4308  iunss  4371  dftr2  4547  axpweq  4629  axpow2  4632  ssextss  4706  ssrel  5096  ssrel2  5098  ssrelrel  5108  reliun  5128  relop  5158  issref  5385  funimass4  5924  dfom2  6702  inf2  8061  grothpw  9225  grothprim  9233  psslinpr  9430  ltaddpr  9433  isprm2  14225  vdwmc2  14497  acsmapd  15808  bwthOLD  19911  dfcon2  19920  iskgen3  20050  metcld  21744  metcld2  21745  isch2  26141  pjnormssi  27087  ssiun3  27426  ssrelf  27466  dffr5  29182  brsset  29539  sscoid  29563  conss34  31351  icccncfext  31690  sbcssOLD  33313  onfrALTlem2  33318  trsspwALT  33616  trsspwALT2  33617  snssiALTVD  33627  snssiALT  33628  sstrALT2VD  33634  sstrALT2  33635  sbcssgVD  33683  onfrALTlem2VD  33689  sspwimp  33718  sspwimpVD  33719  sspwimpcf  33720  sspwimpcfVD  33721  sspwimpALT  33725  unisnALT  33726  bnj1361  33887  bnj978  34007  rp-fakeinunass  37740  dfss6  37792  dfhe3  37799  snhesn  37809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator