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

Definition df-ss 2904
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that AA (proved in ssid 2937). Contrast this relationship with the relationship AB (as will be defined in df-pss 2906). For a more traditional definition, but requiring a dummy variable, see dfss2 2907 (or dfss3 2908 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 2890 . 2 wff AB
41, 2cin 2889 . . 3 class (AB)
54, 1wceq 1226 . 2 wff (AB) = A
63, 5wb 98 1 wff (AB ↔ (AB) = A)
Colors of variables: wff set class
This definition is referenced by:  dfss  2905  dfss1  3114  inabs  3141  nssinpss  3142  dfrab3ss  3188  disjssun  3258  riinm  3699  rintm  3714  ssex  3864  op1stb  4155  op1stbg  4156  ssdmres  4556  resima2  4567  xpssres  4568  fnimaeq0  4942  fnreseql  5198  tpostpos2  5798  tfrexlem  5866  ecinxp  6088  bdssex  7264
  Copyright terms: Public domain W3C validator