Theorem eqvreldisj1

Description: The elements of the quotient set of an equivalence relation are disjoint (cf. eqvreldisj2 , eqvreldisj3 ). (Contributed by Mario Carneiro, 10-Dec-2016) (Revised by Peter Mazsa, 3-Dec-2024)

	Ref	Expression
Assertion	eqvreldisj1	⊢ ( EqvRel 𝑅 → ∀ 𝑥 ∈ ( 𝐴 / 𝑅 ) ∀ 𝑦 ∈ ( 𝐴 / 𝑅 ) ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( EqvRel 𝑅 ∧ ( 𝑥 ∈ ( 𝐴 / 𝑅 ) ∧ 𝑦 ∈ ( 𝐴 / 𝑅 ) ) ) → EqvRel 𝑅 )
2		simprl	⊢ ( ( EqvRel 𝑅 ∧ ( 𝑥 ∈ ( 𝐴 / 𝑅 ) ∧ 𝑦 ∈ ( 𝐴 / 𝑅 ) ) ) → 𝑥 ∈ ( 𝐴 / 𝑅 ) )
3		simprr	⊢ ( ( EqvRel 𝑅 ∧ ( 𝑥 ∈ ( 𝐴 / 𝑅 ) ∧ 𝑦 ∈ ( 𝐴 / 𝑅 ) ) ) → 𝑦 ∈ ( 𝐴 / 𝑅 ) )
4	1 2 3	qsdisjALTV	⊢ ( ( EqvRel 𝑅 ∧ ( 𝑥 ∈ ( 𝐴 / 𝑅 ) ∧ 𝑦 ∈ ( 𝐴 / 𝑅 ) ) ) → ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )
5	4	ralrimivva	⊢ ( EqvRel 𝑅 → ∀ 𝑥 ∈ ( 𝐴 / 𝑅 ) ∀ 𝑦 ∈ ( 𝐴 / 𝑅 ) ( 𝑥 = 𝑦 ∨ ( 𝑥 ∩ 𝑦 ) = ∅ ) )