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

Definition df-ss 3084
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴𝐴 (proved in ssid 3117). For a more traditional definition, but requiring a dummy variable, see dfss2 3086. Other possible definitions are given by dfss3 3087, ssequn1 3246, ssequn2 3249, and sseqin2 3295. (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 3071 . 2 wff 𝐴𝐵
41, 2cin 3070 . . 3 class (𝐴𝐵)
54, 1wceq 1331 . 2 wff (𝐴𝐵) = 𝐴
63, 5wb 104 1 wff (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
Colors of variables: wff set class
This definition is referenced by:  dfss  3085  dfss1  3280  inabs  3308  dfrab3ss  3354  disjssun  3426  riinm  3885  rintm  3905  ssex  4065  op1stb  4399  op1stbg  4400  ssdmres  4841  resima2  4853  xpssres  4854  fnimaeq0  5244  f0rn0  5317  fnreseql  5530  tpostpos2  6162  tfrexlem  6231  ecinxp  6504  uzin  9365  iooval2  9705  minmax  11008  xrminmax  11041  2prm  11815  dfphi2  11903  restid2  12139  difopn  12287  restopnb  12360  cnrest2  12415  bdssex  13130
  Copyright terms: Public domain W3C validator