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

Theorem dfss2 3169
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 3167 . . 3  |-  ( A 
C_  B  <->  A  =  ( A  i^i  B ) )
2 df-in 3159 . . . 4  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
32eqeq2i 2293 . . 3  |-  ( A  =  ( A  i^i  B )  <->  A  =  {
x  |  ( x  e.  A  /\  x  e.  B ) } )
4 abeq2 2388 . . 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 1553 . 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 1527    = wceq 1623    e. wcel 1684   {cab 2269    i^i cin 3151    C_ wss 3152
This theorem is referenced by:  dfss3  3170  dfss2f  3171  ssel  3174  ssriv  3184  ssrdv  3185  sstr2  3186  eqss  3194  nss  3236  rabss2  3256  ssconb  3309  ssequn1  3345  unss  3349  ssin  3391  reldisj  3498  ssdif0  3513  difin0ss  3520  inssdif0  3521  ssundif  3537  sbcss  3564  pwss  3639  snss  3748  pwpw0  3763  pwsnALT  3822  ssuni  3849  unissb  3857  intss  3883  iunss  3943  dftr2  4115  axpweq  4187  axpow2  4190  ssextss  4227  dfom2  4658  ssrel  4776  ssrelrel  4787  reliun  4806  relop  4834  issref  5056  funimass4  5573  inf2  7324  grothpw  8448  grothprim  8456  psslinpr  8655  ltaddpr  8658  isprm2  12766  vdwmc2  13026  acsmapd  14281  dfcon2  17145  iskgen3  17244  metcld  18731  metcld2  18732  isch2  21803  pjnormssi  22748  ballotlem2  23047  ssiun3  23156  fzossnn  23278  dffr5  24110  brsset  24429  domfldrefc  25057  ranfldrefc  25058  bwt2  25592  conss34  27645  rrpsscn  27719  stoweidlem59  27808  sbcssOLD  28306  onfrALTlem2  28311  trsspwALT  28592  trsspwALT2  28593  snssiALTVD  28602  snssiALT  28603  sstrALT2VD  28610  sstrALT2  28611  sbcssVD  28659  onfrALTlem2VD  28665  sspwimp  28694  sspwimpVD  28695  sspwimpcf  28696  sspwimpcfVD  28697  sspwimpALT  28701  unisnALT  28702  sspwimpALT2  28705  bnj1361  28861  bnj978  28981
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator