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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ElDisjs ↔ ElDisj 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eleldisjs	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ElDisjs ↔ ( ◡ E ↾ 𝐴 ) ∈ Disjs ) )
2		cnvepresex	⊢ ( 𝐴 ∈ 𝑉 → ( ◡ E ↾ 𝐴 ) ∈ V )
3		eldisjsdisj	⊢ ( ( ◡ E ↾ 𝐴 ) ∈ V → ( ( ◡ E ↾ 𝐴 ) ∈ Disjs ↔ Disj ( ◡ E ↾ 𝐴 ) ) )
4	2 3	syl	⊢ ( 𝐴 ∈ 𝑉 → ( ( ◡ E ↾ 𝐴 ) ∈ Disjs ↔ Disj ( ◡ E ↾ 𝐴 ) ) )
5	1 4	bitrd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ElDisjs ↔ Disj ( ◡ E ↾ 𝐴 ) ) )
6		df-eldisj	⊢ ( ElDisj 𝐴 ↔ Disj ( ◡ E ↾ 𝐴 ) )
7	5 6	bitr4di	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ElDisjs ↔ ElDisj 𝐴 ) )