Theorem eleldisjseldisj

Description: 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. (Contributed by Peter Mazsa, 23-Jul-2023)

	Ref	Expression
Assertion	eleldisjseldisj	$$⊢A\in V\to \left(A\in \mathrm{ElDisjs}\leftrightarrow ElDisjA\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleldisjs	$$⊢A\in V\to \left(A\in \mathrm{ElDisjs}\leftrightarrow {{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{Disjs}\right)$$
2		cnvepresex	$$⊢A\in V\to {{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{V}$$
3		eldisjsdisj	$$⊢{{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{V}\to \left({{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{Disjs}\leftrightarrow Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\right)$$
4	2 3	syl	$$⊢A\in V\to \left({{\mathrm{E}}^{-1}\upharpoonright }_A\in \mathrm{Disjs}\leftrightarrow Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\right)$$
5	1 4	bitrd	$$⊢A\in V\to \left(A\in \mathrm{ElDisjs}\leftrightarrow Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\right)$$
6		df-eldisj	$$⊢ElDisjA\leftrightarrow Disj\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
7	5 6	bitr4di	$$⊢A\in V\to \left(A\in \mathrm{ElDisjs}\leftrightarrow ElDisjA\right)$$