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 -1 ↾ A -1 ⊆ I

Proof

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