Description: Alternate definition of the disjoint elementhood predicate. (Contributed by Peter Mazsa, 19-Sep-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | dfeldisj2 | ⊢ ( ElDisj 𝐴 ↔ ≀ ◡ ( ◡ E ↾ 𝐴 ) ⊆ I ) |
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 ) |