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

Definition df-ss 3026
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴𝐴 (proved in ssid 3059). For a more traditional definition, but requiring a dummy variable, see dfss2 3028. Other possible definitions are given by dfss3 3029, ssequn1 3185, ssequn2 3188, and sseqin2 3234. (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 3013 . 2 wff 𝐴𝐵
41, 2cin 3012 . . 3 class (𝐴𝐵)
54, 1wceq 1296 . 2 wff (𝐴𝐵) = 𝐴
63, 5wb 104 1 wff (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
Colors of variables: wff set class
This definition is referenced by:  dfss  3027  dfss1  3219  inabs  3247  dfrab3ss  3293  disjssun  3365  riinm  3824  rintm  3843  ssex  3997  op1stb  4328  op1stbg  4329  ssdmres  4767  resima2  4779  xpssres  4780  fnimaeq0  5169  f0rn0  5240  fnreseql  5448  tpostpos2  6068  tfrexlem  6137  ecinxp  6407  uzin  9150  iooval2  9481  minmax  10792  xrminmax  10824  2prm  11551  dfphi2  11638  restid2  11828  difopn  11975  restopnb  12048  cnrest2  12102  bdssex  12505
  Copyright terms: Public domain W3C validator