Definition df-eldisjs

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 ( A e. ElDisjs <-> ElDisj A ) when A is a set, see eleldisjseldisj . (Contributed by Peter Mazsa, 28-Nov-2022)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		celdisjs	⊢ ElDisjs
1		va	⊢ 𝑎
2		cep	⊢ E
3	2	ccnv	⊢ ◡ E
4	1	cv	⊢ 𝑎
5	3 4	cres	⊢ ( ◡ E ↾ 𝑎 )
6		cdisjs	⊢ Disjs
7	5 6	wcel	⊢ ( ◡ E ↾ 𝑎 ) ∈ Disjs
8	7 1	cab	⊢ { 𝑎 ∣ ( ◡ E ↾ 𝑎 ) ∈ Disjs }
9	0 8	wceq	⊢ ElDisjs = { 𝑎 ∣ ( ◡ E ↾ 𝑎 ) ∈ Disjs }