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 A ⊆ A (proved in ssid 2958). Contrast this relationship with the relationship A ⊊ B (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  8281  iooval2  8554  bdssex  9357
 Copyright terms: Public domain W3C validator