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

Definition df-ss 3084
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that  A  C_  A (proved in ssid 3117). For a more traditional definition, but requiring a dummy variable, see dfss2 3086. Other possible definitions are given by dfss3 3087, ssequn1 3246, ssequn2 3249, and sseqin2 3295. (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 3071 . 2  wff  A  C_  B
41, 2cin 3070 . . 3  class  ( A  i^i  B )
54, 1wceq 1331 . 2  wff  ( A  i^i  B )  =  A
63, 5wb 104 1  wff  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
Colors of variables: wff set class
This definition is referenced by:  dfss  3085  dfss1  3280  inabs  3308  dfrab3ss  3354  disjssun  3426  riinm  3885  rintm  3905  ssex  4065  op1stb  4399  op1stbg  4400  ssdmres  4841  resima2  4853  xpssres  4854  fnimaeq0  5244  f0rn0  5317  fnreseql  5530  tpostpos2  6162  tfrexlem  6231  ecinxp  6504  uzin  9372  iooval2  9712  minmax  11015  xrminmax  11048  2prm  11821  dfphi2  11909  restid2  12145  difopn  12293  restopnb  12366  cnrest2  12421  bdssex  13207
  Copyright terms: Public domain W3C validator