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

Theorem dfss2 3450
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 3448 . . 3  |-  ( A 
C_  B  <->  A  =  ( A  i^i  B ) )
2 df-in 3440 . . . 4  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
32eqeq2i 2438 . . 3  |-  ( A  =  ( A  i^i  B )  <->  A  =  {
x  |  ( x  e.  A  /\  x  e.  B ) } )
4 abeq2 2544 . . 3  |-  ( A  =  { x  |  ( x  e.  A  /\  x  e.  B
) }  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  x  e.  B )
) )
51, 3, 43bitri 274 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  x  e.  B )
) )
6 pm4.71 634 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  ( x  e.  A  <->  ( x  e.  A  /\  x  e.  B ) ) )
76albii 1687 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  x  e.  B )
) )
85, 7bitr4i 255 1  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370   A.wal 1435    = wceq 1437    e. wcel 1867   {cab 2405    i^i cin 3432    C_ wss 3433
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-in 3440  df-ss 3447
This theorem is referenced by:  dfss3  3451  dfss2f  3452  ssel  3455  ssriv  3465  ssrdv  3467  sstr2  3468  eqss  3476  nss  3519  rabss2  3541  ssconb  3595  ssequn1  3633  unss  3637  ssin  3681  reldisj  3833  ssdif0  3848  difin0ss  3858  inssdif0  3859  ssundif  3876  sbcssg  3905  pwss  3991  snss  4118  pwpw0  4142  pwsnALT  4208  ssuni  4235  unissb  4244  intssOLD  4271  iunss  4334  dftr2  4514  axpweq  4594  axpow2  4597  ssextss  4668  ssrel  4935  ssrel2  4937  ssrelrel  4947  reliun  4966  relop  4997  issref  5225  funimass4  5924  dfom2  6700  inf2  8126  grothpw  9247  grothprim  9255  psslinpr  9452  ltaddpr  9455  isprm2  14610  vdwmc2  14907  acsmapd  16402  dfcon2  20411  iskgen3  20541  metcld  22252  metcld2  22253  isch2  26852  pjnormssi  27797  ssiun3  28153  ssrelf  28201  bnj1361  29629  bnj978  29749  dffr5  30381  brsset  30642  sscoid  30666  relowlpssretop  31702  rp-fakeinunass  36074  ss2iundf  36105  dfss6  36215  dfhe3  36222  snhesn  36234  dffrege76  36387  conss34  36647  sbcssOLD  36759  onfrALTlem2  36764  trsspwALT  37061  trsspwALT2  37062  snssiALTVD  37078  snssiALT  37079  sstrALT2VD  37085  sstrALT2  37086  sbcssgVD  37135  onfrALTlem2VD  37141  sspwimp  37170  sspwimpVD  37171  sspwimpcf  37172  sspwimpcfVD  37173  sspwimpALT  37177  unisnALT  37178  icccncfext  37552
  Copyright terms: Public domain W3C validator