Description: The element of the disjoint elements class and the disjoint elementhood predicate are the same, that is ( A e. ElDisjs <-> ElDisj A ) when A is a set. (Contributed by Peter Mazsa, 23-Jul-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | eleldisjseldisj | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ElDisjs ↔ ElDisj 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleldisjs | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ElDisjs ↔ ( ◡ E ↾ 𝐴 ) ∈ Disjs ) ) | |
2 | cnvepresex | ⊢ ( 𝐴 ∈ 𝑉 → ( ◡ E ↾ 𝐴 ) ∈ V ) | |
3 | eldisjsdisj | ⊢ ( ( ◡ E ↾ 𝐴 ) ∈ V → ( ( ◡ E ↾ 𝐴 ) ∈ Disjs ↔ Disj ( ◡ E ↾ 𝐴 ) ) ) | |
4 | 2 3 | syl | ⊢ ( 𝐴 ∈ 𝑉 → ( ( ◡ E ↾ 𝐴 ) ∈ Disjs ↔ Disj ( ◡ E ↾ 𝐴 ) ) ) |
5 | 1 4 | bitrd | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ElDisjs ↔ Disj ( ◡ E ↾ 𝐴 ) ) ) |
6 | df-eldisj | ⊢ ( ElDisj 𝐴 ↔ Disj ( ◡ E ↾ 𝐴 ) ) | |
7 | 5 6 | bitr4di | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ElDisjs ↔ ElDisj 𝐴 ) ) |