This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eleldisjs

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

Ref Expression
Assertion eleldisjs ⊢ A ∈ V → A ∈ ElDisjs ↔ E -1 ↾ A ∈ Disjs

Proof

Step Hyp Ref Expression
1 reseq2 ⊢ a = A → E -1 ↾ a = E -1 ↾ A
2 1 eleq1d ⊢ a = A → E -1 ↾ a ∈ Disjs ↔ E -1 ↾ A ∈ Disjs
3 df-eldisjs ⊢ ElDisjs = a | E -1 ↾ a ∈ Disjs
4 2 3 elab2g ⊢ A ∈ V → A ∈ ElDisjs ↔ E -1 ↾ A ∈ Disjs