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

Theorem dfss2 3092
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 3090 . . 3  |-  ( A 
C_  B  <->  A  =  ( A  i^i  B ) )
2 df-in 3085 . . . 4  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
32eqeq2i 2263 . . 3  |-  ( A  =  ( A  i^i  B )  <->  A  =  {
x  |  ( x  e.  A  /\  x  e.  B ) } )
4 abeq2 2354 . . 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 614 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  ( x  e.  A  <->  ( x  e.  A  /\  x  e.  B ) ) )
76albii 1554 . 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 6    <-> wb 178    /\ wa 360   A.wal 1532    = wceq 1619    e. wcel 1621   {cab 2239    i^i cin 3077    C_ wss 3078
This theorem is referenced by:  dfss3  3093  dfss2f  3094  ssel  3097  ssriv  3105  ssrdv  3106  sstr2  3107  eqss  3115  nss  3157  rabss2  3177  ssconb  3223  ssequn1  3255  unss  3259  ssin  3298  reldisj  3405  ssdif0  3420  difin0ss  3426  inssdif0  3427  ssundif  3443  pwss  3543  snss  3652  pwpw0  3663  pwsnALT  3722  ssuni  3749  unissb  3755  intss  3781  iunss  3841  dftr2  4012  axpweq  4081  axpow2  4084  ssextss  4121  dfom2  4549  ssrel  4683  ssrelrel  4694  reliun  4713  relop  4741  issref  4963  funimass4  5425  inf2  7208  grothpw  8328  grothprim  8336  psslinpr  8535  ltaddpr  8538  isprm2  12640  vdwmc2  12900  dfcon2  16977  iskgen3  17076  metcld  18563  metcld2  18564  isch2  21633  pjnormssi  22578  dffr5  23280  brsset  23604  domfldrefc  24222  ranfldrefc  24223  bwt2  24758  conss34  26812  sbcss  26999  onfrALTlem2  27004  trsspwALT  27282  trsspwALT2  27283  snssiALTVD  27292  snssiALT  27293  sstrALT2VD  27300  sstrALT2  27301  sbcssVD  27349  onfrALTlem2VD  27355  sspwimp  27384  sspwimpVD  27385  sspwimpcf  27386  sspwimpcfVD  27387  sspwimpALT  27391  unisnALT  27392  sspwimpALT2  27395  bnj1361  27550  bnj978  27670
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator