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	$$⊢\mathrm{ElDisjs}=\left\{a|{{\mathrm{E}}^{-1}\upharpoonright }_a\in \mathrm{Disjs}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		celdisjs	$$class\mathrm{ElDisjs}$$
1		va	$$setvara$$
2		cep	$$class\mathrm{E}$$
3	2	ccnv	$$class{\mathrm{E}}^{-1}$$
4	1	cv	$$setvara$$
5	3 4	cres	$$class\left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)$$
6		cdisjs	$$class\mathrm{Disjs}$$
7	5 6	wcel	$$wff{{\mathrm{E}}^{-1}\upharpoonright }_a\in \mathrm{Disjs}$$
8	7 1	cab	$$class\left\{a|{{\mathrm{E}}^{-1}\upharpoonright }_a\in \mathrm{Disjs}\right\}$$
9	0 8	wceq	$$wff\mathrm{ElDisjs}=\left\{a|{{\mathrm{E}}^{-1}\upharpoonright }_a\in \mathrm{Disjs}\right\}$$