Theorem qsdisj2

Description: A quotient set is a disjoint set. (Contributed by Mario Carneiro, 10-Dec-2016)

	Ref	Expression
Assertion	qsdisj2	|- ( R Er X -> Disj_ x e. ( A /. R ) x )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( R Er X /\ ( x e. ( A /. R ) /\ y e. ( A /. R ) ) ) -> R Er X )
2		simprl	|- ( ( R Er X /\ ( x e. ( A /. R ) /\ y e. ( A /. R ) ) ) -> x e. ( A /. R ) )
3		simprr	|- ( ( R Er X /\ ( x e. ( A /. R ) /\ y e. ( A /. R ) ) ) -> y e. ( A /. R ) )
4	1 2 3	qsdisj	|- ( ( R Er X /\ ( x e. ( A /. R ) /\ y e. ( A /. R ) ) ) -> ( x = y \/ ( x i^i y ) = (/) ) )
5	4	ralrimivva	|- ( R Er X -> A. x e. ( A /. R ) A. y e. ( A /. R ) ( x = y \/ ( x i^i y ) = (/) ) )
6		id	|- ( x = y -> x = y )
7	6	disjor	|- ( Disj_ x e. ( A /. R ) x <-> A. x e. ( A /. R ) A. y e. ( A /. R ) ( x = y \/ ( x i^i y ) = (/) ) )
8	5 7	sylibr	|- ( R Er X -> Disj_ x e. ( A /. R ) x )