Metamath Proof Explorer

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 ⊢ A ∈ V → A ∈ ElDisjs ↔ ElDisj A

Proof

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