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

Definition df-ss 2925
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that AA (proved in ssid 2958). Contrast this relationship with the relationship AB (as will be defined in df-pss 2927). For a more traditional definition, but requiring a dummy variable, see dfss2 2928 (or dfss3 2929 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 2911 . 2 wff AB
41, 2cin 2910 . . 3 class (AB)
54, 1wceq 1242 . 2 wff (AB) = A
63, 5wb 98 1 wff (AB ↔ (AB) = A)
Colors of variables: wff set class
This definition is referenced by:  dfss  2926  dfss1  3135  inabs  3162  nssinpss  3163  dfrab3ss  3209  disjssun  3279  riinm  3720  rintm  3735  ssex  3885  op1stb  4175  op1stbg  4176  ssdmres  4576  resima2  4587  xpssres  4588  fnimaeq0  4963  fnreseql  5220  tpostpos2  5821  tfrexlem  5889  ecinxp  6117  uzin  8241  iooval2  8514  bdssex  9287
  Copyright terms: Public domain W3C validator