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

Theorem dfss2 3339
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  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
Distinct variable groups:    x, A    x, B

Proof of Theorem dfss2
StepHypRef Expression
1 dfss 3337 . . 3  |-  ( A 
C_  B  <->  A  =  ( A  i^i  B ) )
2 df-in 3329 . . . 4  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
32eqeq2i 2448 . . 3  |-  ( A  =  ( A  i^i  B )  <->  A  =  {
x  |  ( x  e.  A  /\  x  e.  B ) } )
4 abeq2 2543 . . 3  |-  ( A  =  { x  |  ( x  e.  A  /\  x  e.  B
) }  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  x  e.  B )
) )
51, 3, 43bitri 264 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  x  e.  B )
) )
6 pm4.71 613 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  ( x  e.  A  <->  ( x  e.  A  /\  x  e.  B ) ) )
76albii 1576 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  x  e.  B )
) )
85, 7bitr4i 245 1  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360   A.wal 1550    = wceq 1653    e. wcel 1726   {cab 2424    i^i cin 3321    C_ wss 3322
This theorem is referenced by:  dfss3  3340  dfss2f  3341  ssel  3344  ssriv  3354  ssrdv  3356  sstr2  3357  eqss  3365  nss  3408  rabss2  3428  ssconb  3482  ssequn1  3519  unss  3523  ssin  3565  reldisj  3673  ssdif0  3688  difin0ss  3696  inssdif0  3697  ssundif  3713  sbcss  3740  pwss  3815  snss  3928  pwpw0  3948  pwsnALT  4012  ssuni  4039  unissb  4047  intss  4073  iunss  4134  dftr2  4306  axpweq  4378  axpow2  4381  ssextss  4419  dfom2  4849  ssrel  4966  ssrel2  4968  ssrelrel  4978  reliun  4997  relop  5025  issref  5249  funimass4  5779  inf2  7580  grothpw  8703  grothprim  8711  psslinpr  8910  ltaddpr  8913  isprm2  13089  vdwmc2  13349  acsmapd  14606  bwth  17475  dfcon2  17484  iskgen3  17583  metcld  19260  metcld2  19261  isch2  22728  pjnormssi  23673  ssiun3  24011  dffr5  25378  brsset  25736  sscoid  25760  conss34  27623  sbcssOLD  28689  onfrALTlem2  28694  trsspwALT  28993  trsspwALT2  28994  snssiALTVD  29001  snssiALT  29002  sstrALT2VD  29008  sstrALT2  29009  sbcssVD  29057  onfrALTlem2VD  29063  sspwimp  29092  sspwimpVD  29093  sspwimpcf  29094  sspwimpcfVD  29095  sspwimpALT  29099  unisnALT  29100  bnj1361  29262  bnj978  29382
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator