Definition df-eldisjs 36796

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 36819. (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 36347	. 2 class ElDisjs
2		cep 5493	. . . . . 6 class E
3	2	ccnv 5587	. . . . 5 class ◡ E
4		va	. . . . . 6 setvar 𝑎
5	4	cv 1540	. . . . 5 class 𝑎
6	3, 5	cres 5590	. . . 4 class (◡ E ↾ 𝑎)
7		cdisjs 36345	. . . 4 class Disjs
8	6, 7	wcel 2109	. . 3 wff (◡ E ↾ 𝑎) ∈ Disjs
9	8, 4	cab 2716	. 2 class {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }
10	1, 9	wceq 1541	1 wff ElDisjs = {𝑎 ∣ (◡ E ↾ 𝑎) ∈ Disjs }

This definition is referenced by:  eleldisjs  36818