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

Metamath Proof Explorer

Theorem elpreq

Description: Equality wihin a pair. (Contributed by Thierry Arnoux, 23-Aug-2017)

Ref Expression
Hypotheses elpreq.1 
|- ( ph -> X e. { A , B } )
elpreq.2 
|- ( ph -> Y e. { A , B } )
elpreq.3 
|- ( ph -> ( X = A <-> Y = A ) )
Assertion elpreq 
|- ( ph -> X = Y )

Proof

Step Hyp Ref Expression
1 elpreq.1 
 |-  ( ph -> X e. { A , B } )
2 elpreq.2 
 |-  ( ph -> Y e. { A , B } )
3 elpreq.3 
 |-  ( ph -> ( X = A <-> Y = A ) )
4 simpr 
 |-  ( ( ph /\ X = A ) -> X = A )
5 3 biimpa 
 |-  ( ( ph /\ X = A ) -> Y = A )
6 4 5 eqtr4d 
 |-  ( ( ph /\ X = A ) -> X = Y )
7 elpri 
 |-  ( X e. { A , B } -> ( X = A \/ X = B ) )
8 1 7 syl 
 |-  ( ph -> ( X = A \/ X = B ) )
9 8 orcanai 
 |-  ( ( ph /\ -. X = A ) -> X = B )
10 simpl 
 |-  ( ( ph /\ -. X = A ) -> ph )
11 3 notbid 
 |-  ( ph -> ( -. X = A <-> -. Y = A ) )
12 11 biimpa 
 |-  ( ( ph /\ -. X = A ) -> -. Y = A )
13 elpri 
 |-  ( Y e. { A , B } -> ( Y = A \/ Y = B ) )
14 pm2.53 
 |-  ( ( Y = A \/ Y = B ) -> ( -. Y = A -> Y = B ) )
15 2 13 14 3syl 
 |-  ( ph -> ( -. Y = A -> Y = B ) )
16 10 12 15 sylc 
 |-  ( ( ph /\ -. X = A ) -> Y = B )
17 9 16 eqtr4d 
 |-  ( ( ph /\ -. X = A ) -> X = Y )
18 6 17 pm2.61dan 
 |-  ( ph -> X = Y )