Metamath Proof Explorer


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 ) )