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∈AB∧A≠B∧A∈V∧B∈V→∃v∈V∖Cv∈AB

Proof

Step Hyp Ref Expression
1 elpri ⊢C∈AB→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∈AB↔B∈AB
13 12 adantl ⊢C=A∧A≠B∧A∈V∧B∈V∧v=B→v∈AB↔B∈AB
14 prid2g ⊢B∈V→B∈AB
15 14 adantl ⊢A∈V∧B∈V→B∈AB
16 15 adantl ⊢A≠B∧A∈V∧B∈V→B∈AB
17 16 adantl ⊢C=A∧A≠B∧A∈V∧B∈V→B∈AB
18 11 13 17 rspcedvd ⊢C=A∧A≠B∧A∈V∧B∈V→∃v∈V∖Cv∈AB
19 18 ex ⊢C=A→A≠B∧A∈V∧B∈V→∃v∈V∖Cv∈AB
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∈AB↔A∈AB
29 28 adantl ⊢C=B∧A≠B∧A∈V∧B∈V∧v=A→v∈AB↔A∈AB
30 prid1g ⊢A∈V→A∈AB
31 30 adantr ⊢A∈V∧B∈V→A∈AB
32 31 adantl ⊢A≠B∧A∈V∧B∈V→A∈AB
33 32 adantl ⊢C=B∧A≠B∧A∈V∧B∈V→A∈AB
34 27 29 33 rspcedvd ⊢C=B∧A≠B∧A∈V∧B∈V→∃v∈V∖Cv∈AB
35 34 ex ⊢C=B→A≠B∧A∈V∧B∈V→∃v∈V∖Cv∈AB
36 19 35 jaoi ⊢C=A∨C=B→A≠B∧A∈V∧B∈V→∃v∈V∖Cv∈AB
37 1 36 syl ⊢C∈AB→A≠B∧A∈V∧B∈V→∃v∈V∖Cv∈AB
38 37 3impib ⊢C∈AB∧A≠B∧A∈V∧B∈V→∃v∈V∖Cv∈AB