# 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 ${⊢}\left({C}\in \left\{{A},{B}\right\}\wedge {A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to \exists {v}\in \left({V}\setminus \left\{{C}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\in \left\{{A},{B}\right\}$

### Proof

Step Hyp Ref Expression
1 elpri ${⊢}{C}\in \left\{{A},{B}\right\}\to \left({C}={A}\vee {C}={B}\right)$
2 simprrr ${⊢}\left({C}={A}\wedge \left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\right)\to {B}\in {V}$
3 necom ${⊢}{A}\ne {B}↔{B}\ne {A}$
4 neeq2 ${⊢}{A}={C}\to \left({B}\ne {A}↔{B}\ne {C}\right)$
5 4 eqcoms ${⊢}{C}={A}\to \left({B}\ne {A}↔{B}\ne {C}\right)$
6 5 biimpcd ${⊢}{B}\ne {A}\to \left({C}={A}\to {B}\ne {C}\right)$
7 3 6 sylbi ${⊢}{A}\ne {B}\to \left({C}={A}\to {B}\ne {C}\right)$
8 7 adantr ${⊢}\left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to \left({C}={A}\to {B}\ne {C}\right)$
9 8 impcom ${⊢}\left({C}={A}\wedge \left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\right)\to {B}\ne {C}$
10 eldifsn ${⊢}{B}\in \left({V}\setminus \left\{{C}\right\}\right)↔\left({B}\in {V}\wedge {B}\ne {C}\right)$
11 2 9 10 sylanbrc ${⊢}\left({C}={A}\wedge \left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\right)\to {B}\in \left({V}\setminus \left\{{C}\right\}\right)$
12 eleq1 ${⊢}{v}={B}\to \left({v}\in \left\{{A},{B}\right\}↔{B}\in \left\{{A},{B}\right\}\right)$
13 12 adantl ${⊢}\left(\left({C}={A}\wedge \left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\right)\wedge {v}={B}\right)\to \left({v}\in \left\{{A},{B}\right\}↔{B}\in \left\{{A},{B}\right\}\right)$
14 prid2g ${⊢}{B}\in {V}\to {B}\in \left\{{A},{B}\right\}$
15 14 adantl ${⊢}\left({A}\in {V}\wedge {B}\in {V}\right)\to {B}\in \left\{{A},{B}\right\}$
16 15 adantl ${⊢}\left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to {B}\in \left\{{A},{B}\right\}$
17 16 adantl ${⊢}\left({C}={A}\wedge \left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\right)\to {B}\in \left\{{A},{B}\right\}$
18 11 13 17 rspcedvd ${⊢}\left({C}={A}\wedge \left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\right)\to \exists {v}\in \left({V}\setminus \left\{{C}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\in \left\{{A},{B}\right\}$
19 18 ex ${⊢}{C}={A}\to \left(\left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to \exists {v}\in \left({V}\setminus \left\{{C}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\in \left\{{A},{B}\right\}\right)$
20 simprrl ${⊢}\left({C}={B}\wedge \left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\right)\to {A}\in {V}$
21 neeq2 ${⊢}{B}={C}\to \left({A}\ne {B}↔{A}\ne {C}\right)$
22 21 eqcoms ${⊢}{C}={B}\to \left({A}\ne {B}↔{A}\ne {C}\right)$
23 22 biimpcd ${⊢}{A}\ne {B}\to \left({C}={B}\to {A}\ne {C}\right)$
24 23 adantr ${⊢}\left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to \left({C}={B}\to {A}\ne {C}\right)$
25 24 impcom ${⊢}\left({C}={B}\wedge \left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\right)\to {A}\ne {C}$
26 eldifsn ${⊢}{A}\in \left({V}\setminus \left\{{C}\right\}\right)↔\left({A}\in {V}\wedge {A}\ne {C}\right)$
27 20 25 26 sylanbrc ${⊢}\left({C}={B}\wedge \left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\right)\to {A}\in \left({V}\setminus \left\{{C}\right\}\right)$
28 eleq1 ${⊢}{v}={A}\to \left({v}\in \left\{{A},{B}\right\}↔{A}\in \left\{{A},{B}\right\}\right)$
29 28 adantl ${⊢}\left(\left({C}={B}\wedge \left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\right)\wedge {v}={A}\right)\to \left({v}\in \left\{{A},{B}\right\}↔{A}\in \left\{{A},{B}\right\}\right)$
30 prid1g ${⊢}{A}\in {V}\to {A}\in \left\{{A},{B}\right\}$
31 30 adantr ${⊢}\left({A}\in {V}\wedge {B}\in {V}\right)\to {A}\in \left\{{A},{B}\right\}$
32 31 adantl ${⊢}\left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to {A}\in \left\{{A},{B}\right\}$
33 32 adantl ${⊢}\left({C}={B}\wedge \left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\right)\to {A}\in \left\{{A},{B}\right\}$
34 27 29 33 rspcedvd ${⊢}\left({C}={B}\wedge \left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\right)\to \exists {v}\in \left({V}\setminus \left\{{C}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\in \left\{{A},{B}\right\}$
35 34 ex ${⊢}{C}={B}\to \left(\left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to \exists {v}\in \left({V}\setminus \left\{{C}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\in \left\{{A},{B}\right\}\right)$
36 19 35 jaoi ${⊢}\left({C}={A}\vee {C}={B}\right)\to \left(\left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to \exists {v}\in \left({V}\setminus \left\{{C}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\in \left\{{A},{B}\right\}\right)$
37 1 36 syl ${⊢}{C}\in \left\{{A},{B}\right\}\to \left(\left({A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to \exists {v}\in \left({V}\setminus \left\{{C}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\in \left\{{A},{B}\right\}\right)$
38 37 3impib ${⊢}\left({C}\in \left\{{A},{B}\right\}\wedge {A}\ne {B}\wedge \left({A}\in {V}\wedge {B}\in {V}\right)\right)\to \exists {v}\in \left({V}\setminus \left\{{C}\right\}\right)\phantom{\rule{.4em}{0ex}}{v}\in \left\{{A},{B}\right\}$