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		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 ) )
3		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 ) )
4	2 3	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 ) )
5	1	breq1d	|- ( x = y -> ( B R z <-> C R z ) )
6	5	rmo4	|- ( E* x e. A B R z <-> A. x e. A A. y e. A ( ( B R z /\ C R z ) -> x = y ) )
7		relelec	|- ( Rel R -> ( z e. [ B ] R <-> B R z ) )
8		relelec	|- ( Rel R -> ( z e. [ C ] R <-> C R z ) )
9	7 8	anbi12d	|- ( Rel R -> ( ( z e. [ B ] R /\ z e. [ C ] R ) <-> ( B R z /\ C R z ) ) )
10	9	imbi1d	|- ( Rel R -> ( ( ( z e. [ B ] R /\ z e. [ C ] R ) -> x = y ) <-> ( ( B R z /\ C R z ) -> x = y ) ) )
11	10	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 ) ) )
12	6 11	bitr4id	|- ( 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 ) ) )
13	12	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 ) ) )
14	4 13	bitr4id	|- ( 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 ) )