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

Theorem dfss2 3171
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 3169 . . 3  |-  ( A 
C_  B  <->  A  =  ( A  i^i  B ) )
2 df-in 3161 . . . 4  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
32eqeq2i 2295 . . 3  |-  ( A  =  ( A  i^i  B )  <->  A  =  {
x  |  ( x  e.  A  /\  x  e.  B ) } )
4 abeq2 2390 . . 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 613 . . 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 1528    = wceq 1624    e. wcel 1685   {cab 2271    i^i cin 3153    C_ wss 3154
This theorem is referenced by:  dfss3  3172  dfss2f  3173  ssel  3176  ssriv  3186  ssrdv  3187  sstr2  3188  eqss  3196  nss  3238  rabss2  3258  ssconb  3311  ssequn1  3347  unss  3351  ssin  3393  reldisj  3500  ssdif0  3515  difin0ss  3522  inssdif0  3523  ssundif  3539  sbcss  3566  pwss  3641  snss  3750  pwpw0  3765  pwsnALT  3824  ssuni  3851  unissb  3859  intss  3885  iunss  3945  dftr2  4117  axpweq  4187  axpow2  4190  ssextss  4227  dfom2  4658  ssrel  4776  ssrelrel  4787  reliun  4806  relop  4834  issref  5056  funimass4  5535  inf2  7320  grothpw  8444  grothprim  8452  psslinpr  8651  ltaddpr  8654  isprm2  12761  vdwmc2  13021  acsmapd  14276  dfcon2  17140  iskgen3  17239  metcld  18726  metcld2  18727  isch2  21796  pjnormssi  22741  ballotlem2  23041  dffr5  23514  brsset  23838  domfldrefc  24456  ranfldrefc  24457  bwt2  24992  conss34  27045  rrpsscn  27119  stoweidlem59  27208  sbcssOLD  27578  onfrALTlem2  27583  trsspwALT  27861  trsspwALT2  27862  snssiALTVD  27871  snssiALT  27872  sstrALT2VD  27879  sstrALT2  27880  sbcssVD  27928  onfrALTlem2VD  27934  sspwimp  27963  sspwimpVD  27964  sspwimpcf  27965  sspwimpcfVD  27966  sspwimpALT  27970  unisnALT  27971  sspwimpALT2  27974  bnj1361  28129  bnj978  28249
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-in 3161  df-ss 3168
  Copyright terms: Public domain W3C validator