Metamath Proof Explorer


Theorem dfdisjs

Description: Alternate definition of the class of disjoints. (Contributed by Peter Mazsa, 18-Jul-2021)

Ref Expression
Assertion dfdisjs Disjs = { 𝑟 ∈ Rels ∣ ≀ 𝑟 ∈ CnvRefRels }

Proof

Step Hyp Ref Expression
1 df-disjs Disjs = ( Disjss ∩ Rels )
2 df-disjss Disjss = { 𝑟 ∣ ≀ 𝑟 ∈ CnvRefRels }
3 1 2 abeqin Disjs = { 𝑟 ∈ Rels ∣ ≀ 𝑟 ∈ CnvRefRels }