Definition df-eldisjs 35979

Description: Define the disjoint elementhood relations class, i.e., the disjoint elements class. The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is (𝐴 ∈ ElDisjs ↔ ElDisj 𝐴) when 𝐴 is a set, see eleldisjseldisj 36002. (Contributed by Peter Mazsa, 28-Nov-2022.)

Assertion

Ref	Expression
df-eldisjs	⊢ ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }

Detailed syntax breakdown of Definition df-eldisjs

Step	Hyp	Ref	Expression
1		celdisjs 35528	. 2 class ElDisjs
2		cep 5457	. . . . . 6 class E
3	2	ccnv 5547	. . . . 5 class ◡ E
4		va	. . . . . 6 setvar 𝑎
5	4	cv 1535	. . . . 5 class 𝑎
6	3, 5	cres 5550	. . . 4 class (◡ E ↾ 𝑎)
7		cdisjs 35526	. . . 4 class Disjs
8	6, 7	wcel 2113	. . 3 wff (◡ E ↾ 𝑎) ∈ Disjs
9	8, 4	cab 2798	. 2 class {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }
10	1, 9	wceq 1536	1 wff ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }

This definition is referenced by:  eleldisjs  36001