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

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 e. V -> ( A e. ElDisjs <-> ElDisj A ) )

Proof

Step Hyp Ref Expression
1 eleldisjs 
 |-  ( A e. V -> ( A e. ElDisjs <-> ( `' _E |` A ) e. Disjs ) )
2 cnvepresex 
 |-  ( A e. V -> ( `' _E |` A ) e. _V )
3 eldisjsdisj 
 |-  ( ( `' _E |` A ) e. _V -> ( ( `' _E |` A ) e. Disjs <-> Disj ( `' _E |` A ) ) )
4 2 3 syl 
 |-  ( A e. V -> ( ( `' _E |` A ) e. Disjs <-> Disj ( `' _E |` A ) ) )
5 1 4 bitrd 
 |-  ( A e. V -> ( A e. ElDisjs <-> Disj ( `' _E |` A ) ) )
6 df-eldisj 
 |-  ( ElDisj A <-> Disj ( `' _E |` A ) )
7 5 6 bitr4di 
 |-  ( A e. V -> ( A e. ElDisjs <-> ElDisj A ) )