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

Definition df-ss 2900
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that AA (proved in ssid 2933). Contrast this relationship with the relationship AB (as will be defined in df-pss 2902). For a more traditional definition, but requiring a dummy variable, see dfss2 2903 (or dfss3 2904 which is similar). (Contributed by NM, 27-Apr-1994.)
Assertion
Ref Expression
df-ss (AB ↔ (AB) = A)

Detailed syntax breakdown of Definition df-ss
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2wss 2886 . 2 wff AB
41, 2cin 2885 . . 3 class (AB)
54, 1wceq 1224 . 2 wff (AB) = A
63, 5wb 98 1 wff (AB ↔ (AB) = A)
Colors of variables: wff set class
This definition is referenced by:  dfss  2901  dfss1  3110  inabs  3137  nssinpss  3138  dfrab3ss  3184  disjssun  3254  riinm  3693  rintm  3708  ssex  3858  op1stb  4148  op1stbg  4149  ssdmres  4549  resima2  4560  xpssres  4561  fnimaeq0  4935  fnreseql  5191  tpostpos2  5791  tfrexlem  5859  ecinxp  6081  bdssex  8355
  Copyright terms: Public domain W3C validator