Metamath Proof Explorer

Theorem 3elpr2eq

Description: If there are three elements in a proper unordered pair, and two of them are different from the third one, the two must be equal. (Contributed by AV, 19-Dec-2021)

Ref Expression
Assertion 3elpr2eq 
|- ( ( ( X e. { A , B } /\ Y e. { A , B } /\ Z e. { A , B } ) /\ ( Y =/= X /\ Z =/= X ) ) -> Y = Z )

Proof

Step Hyp Ref Expression
1 elpri 
 |-  ( X e. { A , B } -> ( X = A \/ X = B ) )
2 elpri 
 |-  ( Y e. { A , B } -> ( Y = A \/ Y = B ) )
3 elpri 
 |-  ( Z e. { A , B } -> ( Z = A \/ Z = B ) )
4 eqtr3 
 |-  ( ( Z = A /\ X = A ) -> Z = X )
5 eqneqall 
 |-  ( Z = X -> ( Z =/= X -> Y = Z ) )
6 4 5 syl 
 |-  ( ( Z = A /\ X = A ) -> ( Z =/= X -> Y = Z ) )
7 6 adantld 
 |-  ( ( Z = A /\ X = A ) -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) )
8 7 ex 
 |-  ( Z = A -> ( X = A -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) )
9 8 a1d 
 |-  ( Z = A -> ( ( Y = A \/ Y = B ) -> ( X = A -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
10 eqtr3 
 |-  ( ( Y = A /\ X = A ) -> Y = X )
11 eqneqall 
 |-  ( Y = X -> ( Y =/= X -> ( Z =/= X -> Y = Z ) ) )
12 10 11 syl 
 |-  ( ( Y = A /\ X = A ) -> ( Y =/= X -> ( Z =/= X -> Y = Z ) ) )
13 12 impd 
 |-  ( ( Y = A /\ X = A ) -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) )
14 13 ex 
 |-  ( Y = A -> ( X = A -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) )
15 14 a1d 
 |-  ( Y = A -> ( Z = B -> ( X = A -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
16 eqtr3 
 |-  ( ( Y = B /\ Z = B ) -> Y = Z )
17 16 2a1d 
 |-  ( ( Y = B /\ Z = B ) -> ( X = A -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) )
18 17 ex 
 |-  ( Y = B -> ( Z = B -> ( X = A -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
19 15 18 jaoi 
 |-  ( ( Y = A \/ Y = B ) -> ( Z = B -> ( X = A -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
20 19 com12 
 |-  ( Z = B -> ( ( Y = A \/ Y = B ) -> ( X = A -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
21 9 20 jaoi 
 |-  ( ( Z = A \/ Z = B ) -> ( ( Y = A \/ Y = B ) -> ( X = A -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
22 21 com13 
 |-  ( X = A -> ( ( Y = A \/ Y = B ) -> ( ( Z = A \/ Z = B ) -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
23 eqtr3 
 |-  ( ( Y = A /\ Z = A ) -> Y = Z )
24 23 2a1d 
 |-  ( ( Y = A /\ Z = A ) -> ( X = B -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) )
25 24 ex 
 |-  ( Y = A -> ( Z = A -> ( X = B -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
26 eqtr3 
 |-  ( ( Y = B /\ X = B ) -> Y = X )
27 26 11 syl 
 |-  ( ( Y = B /\ X = B ) -> ( Y =/= X -> ( Z =/= X -> Y = Z ) ) )
28 27 impd 
 |-  ( ( Y = B /\ X = B ) -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) )
29 28 ex 
 |-  ( Y = B -> ( X = B -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) )
30 29 a1d 
 |-  ( Y = B -> ( Z = A -> ( X = B -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
31 25 30 jaoi 
 |-  ( ( Y = A \/ Y = B ) -> ( Z = A -> ( X = B -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
32 31 com12 
 |-  ( Z = A -> ( ( Y = A \/ Y = B ) -> ( X = B -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
33 eqtr3 
 |-  ( ( Z = B /\ X = B ) -> Z = X )
34 33 5 syl 
 |-  ( ( Z = B /\ X = B ) -> ( Z =/= X -> Y = Z ) )
35 34 adantld 
 |-  ( ( Z = B /\ X = B ) -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) )
36 35 ex 
 |-  ( Z = B -> ( X = B -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) )
37 36 a1d 
 |-  ( Z = B -> ( ( Y = A \/ Y = B ) -> ( X = B -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
38 32 37 jaoi 
 |-  ( ( Z = A \/ Z = B ) -> ( ( Y = A \/ Y = B ) -> ( X = B -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
39 38 com13 
 |-  ( X = B -> ( ( Y = A \/ Y = B ) -> ( ( Z = A \/ Z = B ) -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
40 22 39 jaoi 
 |-  ( ( X = A \/ X = B ) -> ( ( Y = A \/ Y = B ) -> ( ( Z = A \/ Z = B ) -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) ) ) )
41 40 3imp 
 |-  ( ( ( X = A \/ X = B ) /\ ( Y = A \/ Y = B ) /\ ( Z = A \/ Z = B ) ) -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) )
42 1 2 3 41 syl3an 
 |-  ( ( X e. { A , B } /\ Y e. { A , B } /\ Z e. { A , B } ) -> ( ( Y =/= X /\ Z =/= X ) -> Y = Z ) )
43 42 imp 
 |-  ( ( ( X e. { A , B } /\ Y e. { A , B } /\ Z e. { A , B } ) /\ ( Y =/= X /\ Z =/= X ) ) -> Y = Z )