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 𝐴 ↔ ≀ ( 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 )