Description: Elementhood in the disjoint elements class. (Contributed by Peter Mazsa, 23-Jul-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | eleldisjs | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ElDisjs ↔ ( ◡ E ↾ 𝐴 ) ∈ Disjs ) ) |
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 ) ) |