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 R \to \forall x \in (A / R) \forall y \in (A / R) (x = y \lor x \cap y = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (EqvRel R \land (x \in (A / R) \land y \in (A / R))) \to EqvRel R$
2		simprl	$⊢ (EqvRel R \land (x \in (A / R) \land y \in (A / R))) \to x \in (A / R)$
3		simprr	$⊢ (EqvRel R \land (x \in (A / R) \land y \in (A / R))) \to y \in (A / R)$
4	1 2 3	qsdisjALTV	$⊢ (EqvRel R \land (x \in (A / R) \land y \in (A / R))) \to (x = y \lor x \cap y = \emptyset)$
5	4	ralrimivva	$⊢ EqvRel R \to \forall x \in (A / R) \forall y \in (A / R) (x = y \lor x \cap y = \emptyset)$

Metamath Proof Explorer

Theorem eqvreldisj1

Proof