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

Definition df-ss 3001
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴𝐴 (proved in ssid 3033). For a more traditional definition, but requiring a dummy variable, see dfss2 3003. Other possible definitions are given by dfss3 3004, ssequn1 3159, ssequn2 3162, and sseqin2 3208. (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 2988 . 2 wff 𝐴𝐵
41, 2cin 2987 . . 3 class (𝐴𝐵)
54, 1wceq 1287 . 2 wff (𝐴𝐵) = 𝐴
63, 5wb 103 1 wff (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
Colors of variables: wff set class
This definition is referenced by:  dfss  3002  dfss1  3193  inabs  3220  dfrab3ss  3266  disjssun  3334  riinm  3785  rintm  3800  ssex  3951  op1stb  4273  op1stbg  4274  ssdmres  4702  resima2  4713  xpssres  4714  fnimaeq0  5100  f0rn0  5168  fnreseql  5372  tpostpos2  5984  tfrexlem  6053  ecinxp  6319  uzin  8983  iooval2  9265  minmax  10556  2prm  10991  dfphi2  11078  bdssex  11238
  Copyright terms: Public domain W3C validator