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 ( 𝐴𝑉 → ( 𝐴 ∈ ElDisjs ↔ ElDisj 𝐴 ) )

Proof

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