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

Theorem dfss2 3144
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 3142 . . 3  |-  ( A 
C_  B  <->  A  =  ( A  i^i  B ) )
2 df-in 3134 . . . 4  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
32eqeq2i 2268 . . 3  |-  ( A  =  ( A  i^i  B )  <->  A  =  {
x  |  ( x  e.  A  /\  x  e.  B ) } )
4 abeq2 2363 . . 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 2244    i^i cin 3126    C_ wss 3127
This theorem is referenced by:  dfss3  3145  dfss2f  3146  ssel  3149  ssriv  3159  ssrdv  3160  sstr2  3161  eqss  3169  nss  3211  rabss2  3231  ssconb  3284  ssequn1  3320  unss  3324  ssin  3366  reldisj  3473  ssdif0  3488  difin0ss  3495  inssdif0  3496  ssundif  3512  pwss  3613  snss  3722  pwpw0  3737  pwsnALT  3796  ssuni  3823  unissb  3831  intss  3857  iunss  3917  dftr2  4089  axpweq  4159  axpow2  4162  ssextss  4199  dfom2  4630  ssrel  4764  ssrelrel  4775  reliun  4794  relop  4822  issref  5044  funimass4  5507  inf2  7292  grothpw  8416  grothprim  8424  psslinpr  8623  ltaddpr  8626  isprm2  12728  vdwmc2  12988  acsmapd  14243  dfcon2  17107  iskgen3  17206  metcld  18693  metcld2  18694  isch2  21763  pjnormssi  22708  ballotlem2  23008  dffr5  23481  brsset  23805  domfldrefc  24423  ranfldrefc  24424  bwt2  24959  conss34  27013  stoweidlem59  27143  sbcss  27359  onfrALTlem2  27364  trsspwALT  27642  trsspwALT2  27643  snssiALTVD  27652  snssiALT  27653  sstrALT2VD  27660  sstrALT2  27661  sbcssVD  27709  onfrALTlem2VD  27715  sspwimp  27744  sspwimpVD  27745  sspwimpcf  27746  sspwimpcfVD  27747  sspwimpALT  27751  unisnALT  27752  sspwimpALT2  27755  bnj1361  27910  bnj978  28030
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 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-in 3134  df-ss 3141
  Copyright terms: Public domain W3C validator