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 }