Theorem eleldisjs

Description: Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023)

	Ref	Expression
Assertion	eleldisjs	$$⊢A\in V\to \left(A\in \mathrm{ElDisjs}\leftrightarrow {{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{Disjs}\right)$$

Proof

Step	Hyp	Ref	Expression
1		reseq2	$$⊢a=A\to {{\mathrm{E}}^{-1}\upharpoonright }_a={{\mathrm{E}}^{-1}\upharpoonright }_A$$
2	1	eleq1d	$$⊢a=A\to \left({{\mathrm{E}}^{-1}\upharpoonright }_a\in \mathrm{Disjs}\leftrightarrow {{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{Disjs}\right)$$
3		df-eldisjs	$$⊢\mathrm{ElDisjs}=\left\{a|{{\mathrm{E}}^{-1}\upharpoonright }_a\in \mathrm{Disjs}\right\}$$
4	2 3	elab2g	$$⊢A\in V\to \left(A\in \mathrm{ElDisjs}\leftrightarrow {{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{Disjs}\right)$$