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

Definition df-ss 2931
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that  A  C_  A (proved in ssid 2964). Contrast this relationship with the relationship  A  C.  B (as will be defined in df-pss 2933). For a more traditional definition, but requiring a dummy variable, see dfss2 2934 (or dfss3 2935 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 2917 . 2  wff  A  C_  B
41, 2cin 2916 . . 3  class  ( A  i^i  B )
54, 1wceq 1243 . 2  wff  ( A  i^i  B )  =  A
63, 5wb 98 1  wff  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
Colors of variables: wff set class
This definition is referenced by:  dfss  2932  dfss1  3141  inabs  3168  nssinpss  3169  dfrab3ss  3215  disjssun  3285  riinm  3729  rintm  3744  ssex  3894  op1stb  4209  op1stbg  4210  ssdmres  4633  resima2  4644  xpssres  4645  fnimaeq0  5020  fnreseql  5277  tpostpos2  5880  tfrexlem  5948  ecinxp  6181  uzin  8505  iooval2  8784  bdssex  10022
  Copyright terms: Public domain W3C validator