ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dfss2 Unicode version

Theorem dfss2 2989
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 2988 . . 3  |-  ( A 
C_  B  <->  A  =  ( A  i^i  B ) )
2 df-in 2980 . . . 4  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
32eqeq2i 2092 . . 3  |-  ( A  =  ( A  i^i  B )  <->  A  =  {
x  |  ( x  e.  A  /\  x  e.  B ) } )
4 abeq2 2188 . . 3  |-  ( A  =  { x  |  ( x  e.  A  /\  x  e.  B
) }  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  x  e.  B )
) )
51, 3, 43bitri 204 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  x  e.  B )
) )
6 pm4.71 381 . . 3  |-  ( ( x  e.  A  ->  x  e.  B )  <->  ( x  e.  A  <->  ( x  e.  A  /\  x  e.  B ) ) )
76albii 1400 . 2  |-  ( A. x ( x  e.  A  ->  x  e.  B )  <->  A. x
( x  e.  A  <->  ( x  e.  A  /\  x  e.  B )
) )
85, 7bitr4i 185 1  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103   A.wal 1283    = wceq 1285    e. wcel 1434   {cab 2068    i^i cin 2973    C_ wss 2974
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-in 2980  df-ss 2987
This theorem is referenced by:  dfss3  2990  dfss2f  2991  ssel  2994  ssriv  3004  ssrdv  3006  sstr2  3007  eqss  3015  nssr  3058  rabss2  3078  ssconb  3106  ssequn1  3143  unss  3147  ssin  3195  ssddif  3205  reldisj  3302  ssdif0im  3315  inssdif0im  3318  ssundifim  3333  sbcssg  3358  pwss  3405  snss  3524  snsssn  3561  ssuni  3631  unissb  3639  intss  3665  iunss  3727  dftr2  3885  axpweq  3953  axpow2  3958  ssextss  3983  ordunisuc2r  4266  setind  4290  zfregfr  4324  tfi  4331  ssrel  4454  ssrel2  4456  ssrelrel  4466  reliun  4486  relop  4514  issref  4737  funimass4  5256  isprm2  10643  bj-inf2vnlem3  10925  bj-inf2vnlem4  10926
  Copyright terms: Public domain W3C validator