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

Definition df-ss 2958
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that  A  C_  A (proved in ssid 2991). Contrast this relationship with the relationship  A  C.  B (as will be defined in df-pss 2960). For a more traditional definition, but requiring a dummy variable, see dfss2 2961 (or dfss3 2962 which is similar). (Contributed by NM, 27-Apr-1994.)
Assertion
Ref Expression
df-ss  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )

Detailed syntax breakdown of Definition df-ss
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2wss 2944 . 2  wff  A  C_  B
41, 2cin 2943 . . 3  class  ( A  i^i  B )
54, 1wceq 1259 . 2  wff  ( A  i^i  B )  =  A
63, 5wb 102 1  wff  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
Colors of variables: wff set class
This definition is referenced by:  dfss  2959  dfss1  3168  inabs  3195  nssinpss  3196  dfrab3ss  3242  disjssun  3312  riinm  3756  rintm  3771  ssex  3921  op1stb  4236  op1stbg  4237  ssdmres  4660  resima2  4671  xpssres  4672  fnimaeq0  5047  fnreseql  5304  tpostpos2  5910  tfrexlem  5978  ecinxp  6211  uzin  8600  iooval2  8884  bdssex  10395
  Copyright terms: Public domain W3C validator