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

Theorem dfss2 3111
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 3109 . . 3  |-  ( A 
C_  B  <->  A  =  ( A  i^i  B ) )
2 df-in 3101 . . . 4  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
32eqeq2i 2266 . . 3  |-  ( A  =  ( A  i^i  B )  <->  A  =  {
x  |  ( x  e.  A  /\  x  e.  B ) } )
4 abeq2 2361 . . 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 2242    i^i cin 3093    C_ wss 3094
This theorem is referenced by:  dfss3  3112  dfss2f  3113  ssel  3116  ssriv  3126  ssrdv  3127  sstr2  3128  eqss  3136  nss  3178  rabss2  3198  ssconb  3251  ssequn1  3287  unss  3291  ssin  3333  reldisj  3440  ssdif0  3455  difin0ss  3462  inssdif0  3463  ssundif  3479  pwss  3580  snss  3689  pwpw0  3704  pwsnALT  3763  ssuni  3790  unissb  3798  intss  3824  iunss  3884  dftr2  4055  axpweq  4125  axpow2  4128  ssextss  4165  dfom2  4595  ssrel  4729  ssrelrel  4740  reliun  4759  relop  4787  issref  5009  funimass4  5472  inf2  7257  grothpw  8381  grothprim  8389  psslinpr  8588  ltaddpr  8591  isprm2  12693  vdwmc2  12953  acsmapd  14208  dfcon2  17072  iskgen3  17171  metcld  18658  metcld2  18659  isch2  21728  pjnormssi  22673  ballotlem2  22973  dffr5  23446  brsset  23770  domfldrefc  24388  ranfldrefc  24389  bwt2  24924  conss34  26978  stoweidlem59  27108  sbcss  27322  onfrALTlem2  27327  trsspwALT  27605  trsspwALT2  27606  snssiALTVD  27615  snssiALT  27616  sstrALT2VD  27623  sstrALT2  27624  sbcssVD  27672  onfrALTlem2VD  27678  sspwimp  27707  sspwimpVD  27708  sspwimpcf  27709  sspwimpcfVD  27710  sspwimpALT  27714  unisnALT  27715  sspwimpALT2  27718  bnj1361  27873  bnj978  27993
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-in 3101  df-ss 3108
  Copyright terms: Public domain W3C validator