Metamath Proof Explorer

Theorem eldisjim2

Description: Alternate form of eldisjim . (Contributed by Peter Mazsa, 30-Dec-2024)

Ref Expression
Assertion eldisjim2 
|- ( ElDisj A -> EqvRel ~ A )

Proof

Step Hyp Ref Expression
1 disjim 
 |-  ( Disj ( `' _E |` A ) -> EqvRel ,~ ( `' _E |` A ) )
2 df-eldisj 
 |-  ( ElDisj A <-> Disj ( `' _E |` A ) )
3 df-coels 
 |-  ~ A = ,~ ( `' _E |` A )
4 3 eqvreleqi 
 |-  ( EqvRel ~ A <-> EqvRel ,~ ( `' _E |` A ) )
5 1 2 4 3imtr4i 
 |-  ( ElDisj A -> EqvRel ~ A )