Theorem eleldisjs

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

	Ref	Expression
Assertion	eleldisjs	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ElDisjs ↔ ( ◡ E ↾ 𝐴 ) ∈ Disjs ) )

Proof

Step	Hyp	Ref	Expression
1		reseq2	⊢ ( 𝑎 = 𝐴 → ( ◡ E ↾ 𝑎 ) = ( ◡ E ↾ 𝐴 ) )
2	1	eleq1d	⊢ ( 𝑎 = 𝐴 → ( ( ◡ E ↾ 𝑎 ) ∈ Disjs ↔ ( ◡ E ↾ 𝐴 ) ∈ Disjs ) )
3		df-eldisjs	⊢ ElDisjs = { 𝑎 ∣ ( ◡ E ↾ 𝑎 ) ∈ Disjs }
4	2 3	elab2g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ElDisjs ↔ ( ◡ E ↾ 𝐴 ) ∈ Disjs ) )