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

Metamath Proof Explorer

Theorem prproe

Description: For an element of a proper unordered pair of elements of a class V , there is another (different) element of the class V which is an element of the proper pair. (Contributed by AV, 18-Dec-2021)

Ref Expression
Assertion prproe 
|- ( ( C e. { A , B } /\ A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } )

Proof

Step Hyp Ref Expression
1 elpri 
 |-  ( C e. { A , B } -> ( C = A \/ C = B ) )
2 eleq1 
 |-  ( v = B -> ( v e. { A , B } <-> B e. { A , B } ) )
3 simprrr 
 |-  ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B e. V )
4 necom 
 |-  ( A =/= B <-> B =/= A )
5 neeq2 
 |-  ( A = C -> ( B =/= A <-> B =/= C ) )
6 5 eqcoms 
 |-  ( C = A -> ( B =/= A <-> B =/= C ) )
7 6 biimpcd 
 |-  ( B =/= A -> ( C = A -> B =/= C ) )
8 4 7 sylbi 
 |-  ( A =/= B -> ( C = A -> B =/= C ) )
9 8 adantr 
 |-  ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> ( C = A -> B =/= C ) )
10 9 impcom 
 |-  ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B =/= C )
11 3 10 eldifsnd 
 |-  ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B e. ( V \ { C } ) )
12 prid2g 
 |-  ( B e. V -> B e. { A , B } )
13 12 adantl 
 |-  ( ( A e. V /\ B e. V ) -> B e. { A , B } )
14 13 ad2antll 
 |-  ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B e. { A , B } )
15 2 11 14 rspcedvdw 
 |-  ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> E. v e. ( V \ { C } ) v e. { A , B } )
16 15 ex 
 |-  ( C = A -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) )
17 eleq1 
 |-  ( v = A -> ( v e. { A , B } <-> A e. { A , B } ) )
18 simprrl 
 |-  ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A e. V )
19 neeq2 
 |-  ( B = C -> ( A =/= B <-> A =/= C ) )
20 19 eqcoms 
 |-  ( C = B -> ( A =/= B <-> A =/= C ) )
21 20 biimpcd 
 |-  ( A =/= B -> ( C = B -> A =/= C ) )
22 21 adantr 
 |-  ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> ( C = B -> A =/= C ) )
23 22 impcom 
 |-  ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A =/= C )
24 18 23 eldifsnd 
 |-  ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A e. ( V \ { C } ) )
25 prid1g 
 |-  ( A e. V -> A e. { A , B } )
26 25 adantr 
 |-  ( ( A e. V /\ B e. V ) -> A e. { A , B } )
27 26 ad2antll 
 |-  ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A e. { A , B } )
28 17 24 27 rspcedvdw 
 |-  ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> E. v e. ( V \ { C } ) v e. { A , B } )
29 28 ex 
 |-  ( C = B -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) )
30 16 29 jaoi 
 |-  ( ( C = A \/ C = B ) -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) )
31 1 30 syl 
 |-  ( C e. { A , B } -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) )
32 31 3impib 
 |-  ( ( C e. { A , B } /\ A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } )