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

Metamath Proof Explorer

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 ) )