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

Definition df-ss 2997
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that  A  C_  A (proved in ssid 3029). For a more traditional definition, but requiring a dummy variable, see dfss2 2999. Other possible definitions are given by dfss3 3000, ssequn1 3154, ssequn2 3157, and sseqin2 3203. (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 2984 . 2  wff  A  C_  B
41, 2cin 2983 . . 3  class  ( A  i^i  B )
54, 1wceq 1285 . 2  wff  ( A  i^i  B )  =  A
63, 5wb 103 1  wff  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
Colors of variables: wff set class
This definition is referenced by:  dfss  2998  dfss1  3188  inabs  3215  dfrab3ss  3260  disjssun  3328  riinm  3776  rintm  3791  ssex  3941  op1stb  4262  op1stbg  4263  ssdmres  4691  resima2  4702  xpssres  4703  fnimaeq0  5087  f0rn0  5152  fnreseql  5353  tpostpos2  5961  tfrexlem  6030  ecinxp  6296  uzin  8945  iooval2  9227  minmax  10485  2prm  10888  dfphi2  10975  bdssex  11135
  Copyright terms: Public domain W3C validator