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 )