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

Definition df-ss 3054
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that  A  C_  A (proved in ssid 3087). For a more traditional definition, but requiring a dummy variable, see dfss2 3056. Other possible definitions are given by dfss3 3057, ssequn1 3216, ssequn2 3219, and sseqin2 3265. (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 3041 . 2  wff  A  C_  B
41, 2cin 3040 . . 3  class  ( A  i^i  B )
54, 1wceq 1316 . 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  3055  dfss1  3250  inabs  3278  dfrab3ss  3324  disjssun  3396  riinm  3855  rintm  3875  ssex  4035  op1stb  4369  op1stbg  4370  ssdmres  4811  resima2  4823  xpssres  4824  fnimaeq0  5214  f0rn0  5287  fnreseql  5498  tpostpos2  6130  tfrexlem  6199  ecinxp  6472  uzin  9314  iooval2  9653  minmax  10956  xrminmax  10989  2prm  11720  dfphi2  11807  restid2  12040  difopn  12188  restopnb  12261  cnrest2  12316  bdssex  12996
  Copyright terms: Public domain W3C validator