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