This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 R -> A. x e. ( A /. R ) A. y e. ( A /. R ) ( x = y \/ ( x i^i y ) = (/) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( EqvRel R /\ ( x e. ( A /. R ) /\ y e. ( A /. R ) ) ) -> EqvRel R )
2 simprl 
 |-  ( ( EqvRel R /\ ( x e. ( A /. R ) /\ y e. ( A /. R ) ) ) -> x e. ( A /. R ) )
3 simprr 
 |-  ( ( EqvRel R /\ ( x e. ( A /. R ) /\ y e. ( A /. R ) ) ) -> y e. ( A /. R ) )
4 1 2 3 qsdisjALTV 
 |-  ( ( EqvRel R /\ ( x e. ( A /. R ) /\ y e. ( A /. R ) ) ) -> ( x = y \/ ( x i^i y ) = (/) ) )
5 4 ralrimivva 
 |-  ( EqvRel R -> A. x e. ( A /. R ) A. y e. ( A /. R ) ( x = y \/ ( x i^i y ) = (/) ) )