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

Definition df-ss 3001
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that  A  C_  A (proved in ssid 3033). For a more traditional definition, but requiring a dummy variable, see dfss2 3003. Other possible definitions are given by dfss3 3004, ssequn1 3159, ssequn2 3162, and sseqin2 3208. (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 2988 . 2  wff  A  C_  B
41, 2cin 2987 . . 3  class  ( A  i^i  B )
54, 1wceq 1287 . 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  3002  dfss1  3193  inabs  3220  dfrab3ss  3266  disjssun  3334  riinm  3787  rintm  3802  ssex  3953  op1stb  4275  op1stbg  4276  ssdmres  4704  resima2  4715  xpssres  4716  fnimaeq0  5102  f0rn0  5170  fnreseql  5374  tpostpos2  5986  tfrexlem  6055  ecinxp  6321  uzin  8986  iooval2  9268  minmax  10559  2prm  11015  dfphi2  11102  bdssex  11262
  Copyright terms: Public domain W3C validator