Definition df-eldisjs 39691

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 39729. (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 39120	. 2 class ElDisjs
2		cep 5550	. . . . . 6 class E
3	2	ccnv 5650	. . . . 5 class ◡ E
4		va	. . . . . 6 setvar 𝑎
5	4	cv 1569	. . . . 5 class 𝑎
6	3, 5	cres 5653	. . . 4 class (◡ E ↾ 𝑎)
7		cdisjs 39118	. . . 4 class Disjs
8	6, 7	wcel 2145	. . 3 wff (◡ E ↾ 𝑎) ∈ Disjs
9	8, 4	cab 2739	. 2 class {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }
10	1, 9	wceq 1570	1 wff ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }

This definition is used by:  eleldisjs  39728