Metamath Proof Explorer


Theorem dfeldisj2

Description: Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021)

Ref Expression
Assertion dfeldisj2
|- ( ElDisj A <-> ,~ `' ( `' _E |` A ) C_ _I )

Proof

Step Hyp Ref Expression
1 df-eldisj
 |-  ( ElDisj A <-> Disj ( `' _E |` A ) )
2 relres
 |-  Rel ( `' _E |` A )
3 dfdisjALTV2
 |-  ( Disj ( `' _E |` A ) <-> ( ,~ `' ( `' _E |` A ) C_ _I /\ Rel ( `' _E |` A ) ) )
4 2 3 mpbiran2
 |-  ( Disj ( `' _E |` A ) <-> ,~ `' ( `' _E |` A ) C_ _I )
5 1 4 bitri
 |-  ( ElDisj A <-> ,~ `' ( `' _E |` A ) C_ _I )