Theorem inecmo

Description: Equivalence of a double restricted universal quantification and a restricted "at most one" inside a universal quantification. (Contributed by Peter Mazsa, 29-May-2018)

	Ref	Expression
Hypothesis	inecmo.1	|- ( x = y -> B = C )
Assertion	inecmo	|- ( Rel R -> ( A. x e. A A. y e. A ( x = y \/ ( [ B ] R i^i [ C ] R ) = (/) ) <-> A. z E* x e. A B R z ) )

Proof

Step	Hyp	Ref	Expression
1		inecmo.1	|- ( x = y -> B = C )
2		relelec	|- ( Rel R -> ( z e. [ B ] R <-> B R z ) )
3		relelec	|- ( Rel R -> ( z e. [ C ] R <-> C R z ) )
4	2 3	anbi12d	|- ( Rel R -> ( ( z e. [ B ] R /\ z e. [ C ] R ) <-> ( B R z /\ C R z ) ) )
5	4	imbi1d	|- ( Rel R -> ( ( ( z e. [ B ] R /\ z e. [ C ] R ) -> x = y ) <-> ( ( B R z /\ C R z ) -> x = y ) ) )
6	5	2ralbidv	|- ( Rel R -> ( A. x e. A A. y e. A ( ( z e. [ B ] R /\ z e. [ C ] R ) -> x = y ) <-> A. x e. A A. y e. A ( ( B R z /\ C R z ) -> x = y ) ) )
7	1	breq1d	|- ( x = y -> ( B R z <-> C R z ) )
8	7	rmo4	|- ( E* x e. A B R z <-> A. x e. A A. y e. A ( ( B R z /\ C R z ) -> x = y ) )
9	6 8	syl6rbbr	|- ( Rel R -> ( E* x e. A B R z <-> A. x e. A A. y e. A ( ( z e. [ B ] R /\ z e. [ C ] R ) -> x = y ) ) )
10	9	albidv	|- ( Rel R -> ( A. z E* x e. A B R z <-> A. z A. x e. A A. y e. A ( ( z e. [ B ] R /\ z e. [ C ] R ) -> x = y ) ) )
11		ineleq	|- ( A. x e. A A. y e. A ( x = y \/ ( [ B ] R i^i [ C ] R ) = (/) ) <-> A. x e. A A. z A. y e. A ( ( z e. [ B ] R /\ z e. [ C ] R ) -> x = y ) )
12		ralcom4	|- ( A. x e. A A. z A. y e. A ( ( z e. [ B ] R /\ z e. [ C ] R ) -> x = y ) <-> A. z A. x e. A A. y e. A ( ( z e. [ B ] R /\ z e. [ C ] R ) -> x = y ) )
13	11 12	bitri	|- ( A. x e. A A. y e. A ( x = y \/ ( [ B ] R i^i [ C ] R ) = (/) ) <-> A. z A. x e. A A. y e. A ( ( z e. [ B ] R /\ z e. [ C ] R ) -> x = y ) )
14	10 13	syl6rbbr	|- ( Rel R -> ( A. x e. A A. y e. A ( x = y \/ ( [ B ] R i^i [ C ] R ) = (/) ) <-> A. z E* x e. A B R z ) )