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

Definition df-ss 3144
Description: Define the subclass relationship. Exercise 9 of [TakeutiZaring] p. 18. Note that 𝐴𝐴 (proved in ssid 3177). For a more traditional definition, but requiring a dummy variable, see dfss2 3146. Other possible definitions are given by dfss3 3147, ssequn1 3307, ssequn2 3310, and sseqin2 3356. (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 3131 . 2 wff 𝐴𝐵
41, 2cin 3130 . . 3 class (𝐴𝐵)
54, 1wceq 1353 . 2 wff (𝐴𝐵) = 𝐴
63, 5wb 105 1 wff (𝐴𝐵 ↔ (𝐴𝐵) = 𝐴)
Colors of variables: wff set class
This definition is referenced by:  dfss  3145  dfss1  3341  inabs  3369  dfrab3ss  3415  disjssun  3488  riinm  3961  rintm  3981  ssex  4142  op1stb  4480  op1stbg  4481  ssdmres  4931  resima2  4943  xpssres  4944  fnimaeq0  5339  f0rn0  5412  fnreseql  5629  tpostpos2  6269  tfrexlem  6338  ecinxp  6613  uzin  9563  iooval2  9918  minmax  11241  xrminmax  11276  2prm  12130  dfphi2  12223  ressbas2d  12531  ressval3d  12534  restid2  12703  lidlbas  13601  difopn  13796  restopnb  13869  cnrest2  13924  bdssex  14842
  Copyright terms: Public domain W3C validator