Definition df-eldisjs 38645

Description: Define the disjoint element 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 38668. (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 38155	. 2 class ElDisjs
2		cep 5549	. . . . . 6 class E
3	2	ccnv 5650	. . . . 5 class ◡ E
4		va	. . . . . 6 setvar 𝑎
5	4	cv 1538	. . . . 5 class 𝑎
6	3, 5	cres 5653	. . . 4 class (◡ E ↾ 𝑎)
7		cdisjs 38153	. . . 4 class Disjs
8	6, 7	wcel 2107	. . 3 wff (◡ E ↾ 𝑎) ∈ Disjs
9	8, 4	cab 2712	. 2 class {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }
10	1, 9	wceq 1539	1 wff ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }

This definition is referenced by:  eleldisjs  38667