Definition df-eldisjs 37571

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 37594. (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 37073	. 2 class ElDisjs
2		cep 5579	. . . . . 6 class E
3	2	ccnv 5675	. . . . 5 class ◡ E
4		va	. . . . . 6 setvar 𝑎
5	4	cv 1540	. . . . 5 class 𝑎
6	3, 5	cres 5678	. . . 4 class (◡ E ↾ 𝑎)
7		cdisjs 37071	. . . 4 class Disjs
8	6, 7	wcel 2106	. . 3 wff (◡ E ↾ 𝑎) ∈ Disjs
9	8, 4	cab 2709	. 2 class {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }
10	1, 9	wceq 1541	1 wff ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }

This definition is referenced by:  eleldisjs  37593