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 A B A B A V B V v V C v A B

Proof

Step Hyp Ref Expression
1 elpri C A B C = A C = B
2 eleq1 v = B v A B B A B
3 simprrr C = A A B A V B V B 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 V B V C = A B C
10 9 impcom C = A A B A V B V B C
11 3 10 eldifsnd C = A A B A V B V B V C
12 prid2g B V B A B
13 12 adantl A V B V B A B
14 13 ad2antll C = A A B A V B V B A B
15 2 11 14 rspcedvdw C = A A B A V B V v V C v A B
16 15 ex C = A A B A V B V v V C v A B
17 eleq1 v = A v A B A A B
18 simprrl C = B A B A V B V A 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 V B V C = B A C
23 22 impcom C = B A B A V B V A C
24 18 23 eldifsnd C = B A B A V B V A V C
25 prid1g A V A A B
26 25 adantr A V B V A A B
27 26 ad2antll C = B A B A V B V A A B
28 17 24 27 rspcedvdw C = B A B A V B V v V C v A B
29 28 ex C = B A B A V B V v V C v A B
30 16 29 jaoi C = A C = B A B A V B V v V C v A B
31 1 30 syl C A B A B A V B V v V C v A B
32 31 3impib C A B A B A V B V v V C v A B