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

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

Detailed syntax breakdown of Definition df-ss
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2wss 2914 . 2 wff 𝐴𝐵
41, 2cin 2913 . . 3 class (𝐴𝐵)
54, 1wceq 1243 . 2 wff (𝐴𝐵) = 𝐴
63, 5wb 98 1 wff (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
Colors of variables: wff set class
This definition is referenced by:  dfss  2929  dfss1  3138  inabs  3165  nssinpss  3166  dfrab3ss  3212  disjssun  3282  riinm  3726  rintm  3741  ssex  3891  op1stb  4196  op1stbg  4197  ssdmres  4611  resima2  4622  xpssres  4623  fnimaeq0  4998  fnreseql  5255  tpostpos2  5858  tfrexlem  5926  ecinxp  6159  uzin  8468  iooval2  8742  bdssex  9886
  Copyright terms: Public domain W3C validator