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