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 simprrr ⊢ C = A ∧ A ≠ B ∧ A ∈ V ∧ B ∈ V → B ∈ V
3 necom ⊢ A ≠ B ↔ B ≠ A
4 neeq2 ⊢ A = C → B ≠ A ↔ B ≠ C
5 4 eqcoms ⊢ C = A → B ≠ A ↔ B ≠ C
6 5 biimpcd ⊢ B ≠ A → C = A → B ≠ C
7 3 6 sylbi ⊢ A ≠ B → C = A → B ≠ C
8 7 adantr ⊢ A ≠ B ∧ A ∈ V ∧ B ∈ V → C = A → B ≠ C
9 8 impcom ⊢ C = A ∧ A ≠ B ∧ A ∈ V ∧ B ∈ V → B ≠ C
10 eldifsn ⊢ B ∈ V ∖ C ↔ B ∈ V ∧ B ≠ C
11 2 9 10 sylanbrc ⊢ C = A ∧ A ≠ B ∧ A ∈ V ∧ B ∈ V → B ∈ V ∖ C
12 eleq1 ⊢ v = B → v ∈ A B ↔ B ∈ A B
13 12 adantl ⊢ C = A ∧ A ≠ B ∧ A ∈ V ∧ B ∈ V ∧ v = B → v ∈ A B ↔ B ∈ A B
14 prid2g ⊢ B ∈ V → B ∈ A B
15 14 adantl ⊢ A ∈ V ∧ B ∈ V → B ∈ A B
16 15 adantl ⊢ A ≠ B ∧ A ∈ V ∧ B ∈ V → B ∈ A B
17 16 adantl ⊢ C = A ∧ A ≠ B ∧ A ∈ V ∧ B ∈ V → B ∈ A B
18 11 13 17 rspcedvd ⊢ C = A ∧ A ≠ B ∧ A ∈ V ∧ B ∈ V → ∃ v ∈ V ∖ C v ∈ A B
19 18 ex ⊢ C = A → A ≠ B ∧ A ∈ V ∧ B ∈ V → ∃ v ∈ V ∖ C v ∈ A B
20 simprrl ⊢ C = B ∧ A ≠ B ∧ A ∈ V ∧ B ∈ V → A ∈ V
21 neeq2 ⊢ B = C → A ≠ B ↔ A ≠ C
22 21 eqcoms ⊢ C = B → A ≠ B ↔ A ≠ C
23 22 biimpcd ⊢ A ≠ B → C = B → A ≠ C
24 23 adantr ⊢ A ≠ B ∧ A ∈ V ∧ B ∈ V → C = B → A ≠ C
25 24 impcom ⊢ C = B ∧ A ≠ B ∧ A ∈ V ∧ B ∈ V → A ≠ C
26 eldifsn ⊢ A ∈ V ∖ C ↔ A ∈ V ∧ A ≠ C
27 20 25 26 sylanbrc ⊢ C = B ∧ A ≠ B ∧ A ∈ V ∧ B ∈ V → A ∈ V ∖ C
28 eleq1 ⊢ v = A → v ∈ A B ↔ A ∈ A B
29 28 adantl ⊢ C = B ∧ A ≠ B ∧ A ∈ V ∧ B ∈ V ∧ v = A → v ∈ A B ↔ A ∈ A B
30 prid1g ⊢ A ∈ V → A ∈ A B
31 30 adantr ⊢ A ∈ V ∧ B ∈ V → A ∈ A B
32 31 adantl ⊢ A ≠ B ∧ A ∈ V ∧ B ∈ V → A ∈ A B
33 32 adantl ⊢ C = B ∧ A ≠ B ∧ A ∈ V ∧ B ∈ V → A ∈ A B
34 27 29 33 rspcedvd ⊢ C = B ∧ A ≠ B ∧ A ∈ V ∧ B ∈ V → ∃ v ∈ V ∖ C v ∈ A B
35 34 ex ⊢ C = B → A ≠ B ∧ A ∈ V ∧ B ∈ V → ∃ v ∈ V ∖ C v ∈ A B
36 19 35 jaoi ⊢ C = A ∨ C = B → A ≠ B ∧ A ∈ V ∧ B ∈ V → ∃ v ∈ V ∖ C v ∈ A B
37 1 36 syl ⊢ C ∈ A B → A ≠ B ∧ A ∈ V ∧ B ∈ V → ∃ v ∈ V ∖ C v ∈ A B
38 37 3impib ⊢ C ∈ A B ∧ A ≠ B ∧ A ∈ V ∧ B ∈ V → ∃ v ∈ V ∖ C v ∈ A B