Description: Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | dfdisjs | ⊢ Disjs = { 𝑟 ∈ Rels ∣ ≀ ◡ 𝑟 ∈ CnvRefRels } |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-disjs | ⊢ Disjs = ( Disjss ∩ Rels ) | |
2 | df-disjss | ⊢ Disjss = { 𝑟 ∣ ≀ ◡ 𝑟 ∈ CnvRefRels } | |
3 | 1 2 | abeqin | ⊢ Disjs = { 𝑟 ∈ Rels ∣ ≀ ◡ 𝑟 ∈ CnvRefRels } |