Theorem dfdisjs3

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

	Ref	Expression
Assertion	dfdisjs3	⊢ Disjs = { 𝑟 ∈ Rels ∣ ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑢 𝑟 𝑥 ∧ 𝑣 𝑟 𝑥 ) → 𝑢 = 𝑣 ) }

Proof

Step	Hyp	Ref	Expression
1		dfdisjs2	⊢ Disjs = { 𝑟 ∈ Rels ∣ ≀ ◡ 𝑟 ⊆ I }
2		cosscnvssid3	⊢ ( ≀ ◡ 𝑟 ⊆ I ↔ ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑢 𝑟 𝑥 ∧ 𝑣 𝑟 𝑥 ) → 𝑢 = 𝑣 ) )
3	1 2	rabbieq	⊢ Disjs = { 𝑟 ∈ Rels ∣ ∀ 𝑢 ∀ 𝑣 ∀ 𝑥 ( ( 𝑢 𝑟 𝑥 ∧ 𝑣 𝑟 𝑥 ) → 𝑢 = 𝑣 ) }