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

Theorem dfss2 3182
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 3180 . . 3  |-  ( A 
C_  B  <->  A  =  ( A  i^i  B ) )
2 df-in 3172 . . . 4  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
32eqeq2i 2306 . . 3  |-  ( A  =  ( A  i^i  B )  <->  A  =  {
x  |  ( x  e.  A  /\  x  e.  B ) } )
4 abeq2 2401 . . 3  |-  ( A  =  { x  |  ( x  e.  A  /\  x  e.  B
) }  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  x  e.  B )
) )
51, 3, 43bitri 262 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  x  e.  B )
) )
6 pm4.71 611 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  ( x  e.  A  <->  ( x  e.  A  /\  x  e.  B ) ) )
76albii 1556 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  x  e.  B )
) )
85, 7bitr4i 243 1  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1530    = wceq 1632    e. wcel 1696   {cab 2282    i^i cin 3164    C_ wss 3165
This theorem is referenced by:  dfss3  3183  dfss2f  3184  ssel  3187  ssriv  3197  ssrdv  3198  sstr2  3199  eqss  3207  nss  3249  rabss2  3269  ssconb  3322  ssequn1  3358  unss  3362  ssin  3404  reldisj  3511  ssdif0  3526  difin0ss  3533  inssdif0  3534  ssundif  3550  sbcss  3577  pwss  3652  snss  3761  pwpw0  3779  pwsnALT  3838  ssuni  3865  unissb  3873  intss  3899  iunss  3959  dftr2  4131  axpweq  4203  axpow2  4206  ssextss  4243  dfom2  4674  ssrel  4792  ssrelrel  4803  reliun  4822  relop  4850  issref  5072  funimass4  5589  inf2  7340  grothpw  8464  grothprim  8472  psslinpr  8671  ltaddpr  8674  isprm2  12782  vdwmc2  13042  acsmapd  14297  dfcon2  17161  iskgen3  17260  metcld  18747  metcld2  18748  isch2  21819  pjnormssi  22764  ballotlem2  23063  ssiun3  23172  fzossnn  23293  dffr5  24181  brsset  24500  domfldrefc  25160  ranfldrefc  25161  bwt2  25695  conss34  27748  rrpsscn  27822  stoweidlem59  27911  sbcssOLD  28605  onfrALTlem2  28610  trsspwALT  28908  trsspwALT2  28909  snssiALTVD  28918  snssiALT  28919  sstrALT2VD  28926  sstrALT2  28927  sbcssVD  28975  onfrALTlem2VD  28981  sspwimp  29010  sspwimpVD  29011  sspwimpcf  29012  sspwimpcfVD  29013  sspwimpALT  29017  unisnALT  29018  sspwimpALT2  29021  bnj1361  29177  bnj978  29297
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator