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 )