Theorem dfeldisj2

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

	Ref	Expression
Assertion	dfeldisj2	⊢ ( ElDisj 𝐴 ↔ ≀ ◡ ( ◡ E ↾ 𝐴 ) ⊆ I )

Proof

Step	Hyp	Ref	Expression
1		df-eldisj	⊢ ( ElDisj 𝐴 ↔ Disj ( ◡ E ↾ 𝐴 ) )
2		relres	⊢ Rel ( ◡ E ↾ 𝐴 )
3		dfdisjALTV2	⊢ ( Disj ( ◡ E ↾ 𝐴 ) ↔ ( ≀ ◡ ( ◡ E ↾ 𝐴 ) ⊆ I ∧ Rel ( ◡ E ↾ 𝐴 ) ) )
4	2 3	mpbiran2	⊢ ( Disj ( ◡ E ↾ 𝐴 ) ↔ ≀ ◡ ( ◡ E ↾ 𝐴 ) ⊆ I )
5	1 4	bitri	⊢ ( ElDisj 𝐴 ↔ ≀ ◡ ( ◡ E ↾ 𝐴 ) ⊆ I )