Metamath Proof Explorer

Theorem eqvreldisj2

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

		Ref	Expression
	Assertion	eqvreldisj2	\|- ( EqvRel R -> ElDisj ( A /. R ) )

Proof

Step	Hyp	Ref	Expression
1		eqvreldisj1	\|- ( EqvRel R -> A. x e. ( A /. R ) A. y e. ( A /. R ) ( x = y \/ ( x i^i y ) = (/) ) )
2		dfeldisj5	\|- ( ElDisj ( A /. R ) <-> A. x e. ( A /. R ) A. y e. ( A /. R ) ( x = y \/ ( x i^i y ) = (/) ) )
3	1 2	sylibr	\|- ( EqvRel R -> ElDisj ( A /. R ) )

Step

Hyp

Ref

Expression

eqvreldisj1

 |-  ( EqvRel R -> A. x e. ( A /. R ) A. y e. ( A /. R ) ( x = y \/ ( x i^i y ) = (/) ) )

dfeldisj5

 |-  ( ElDisj ( A /. R ) <-> A. x e. ( A /. R ) A. y e. ( A /. R ) ( x = y \/ ( x i^i y ) = (/) ) )

1 2

sylibr

 |-  ( EqvRel R -> ElDisj ( A /. R ) )