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

Definition df-ss 2987
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴𝐴 (proved in ssid 3019). For a more traditional definition, but requiring a dummy variable, see dfss2 2989. Other possible definitions are given by dfss3 2990, ssequn1 3143, ssequn2 3146, and sseqin2 3192. (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 2974 . 2 wff 𝐴𝐵
41, 2cin 2973 . . 3 class (𝐴𝐵)
54, 1wceq 1285 . 2 wff (𝐴𝐵) = 𝐴
63, 5wb 103 1 wff (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
Colors of variables: wff set class
This definition is referenced by:  dfss  2988  dfss1  3177  inabs  3204  dfrab3ss  3249  disjssun  3314  riinm  3758  rintm  3773  ssex  3923  op1stb  4235  op1stbg  4236  ssdmres  4661  resima2  4672  xpssres  4673  fnimaeq0  5051  fnreseql  5309  tpostpos2  5914  tfrexlem  5983  ecinxp  6247  uzin  8732  iooval2  9014  minmax  10250  2prm  10653  bdssex  10851
  Copyright terms: Public domain W3C validator