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 = { a | ( `' _E |` a ) e. Disjs }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		celdisjs	|- ElDisjs
1		va	|- a
2		cep	|- _E
3	2	ccnv	|- `' _E
4	1	cv	|- a
5	3 4	cres	|- ( `' _E |` a )
6		cdisjs	|- Disjs
7	5 6	wcel	|- ( `' _E |` a ) e. Disjs
8	7 1	cab	|- { a | ( `' _E |` a ) e. Disjs }
9	0 8	wceq	|- ElDisjs = { a | ( `' _E |` a ) e. Disjs }