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 e. V -> ( A e. ElDisjs <-> ElDisj A ) )

Proof

Step	Hyp	Ref	Expression
1		eleldisjs	|- ( A e. V -> ( A e. ElDisjs <-> ( `' _E |` A ) e. Disjs ) )
2		cnvepresex	|- ( A e. V -> ( `' _E |` A ) e. _V )
3		eldisjsdisj	|- ( ( `' _E |` A ) e. _V -> ( ( `' _E |` A ) e. Disjs <-> Disj ( `' _E |` A ) ) )
4	2 3	syl	|- ( A e. V -> ( ( `' _E |` A ) e. Disjs <-> Disj ( `' _E |` A ) ) )
5	1 4	bitrd	|- ( A e. V -> ( A e. ElDisjs <-> Disj ( `' _E |` A ) ) )
6		df-eldisj	|- ( ElDisj A <-> Disj ( `' _E |` A ) )
7	5 6	bitr4di	|- ( A e. V -> ( A e. ElDisjs <-> ElDisj A ) )