Metamath Proof Explorer

Theorem exprelprel

Description: If there is an element of the set of subsets with two elements in a set, an unordered pair of sets is in the set. (Contributed by Alexander van der Vekens, 12-Jul-2018)

Ref Expression
Assertion exprelprel ⊢ ∃ p ∈ e ∈ 𝒫 V | e = 2 p ∈ X → ∃ v ∈ V ∃ w ∈ V v w ∈ X

Proof

Step Hyp Ref Expression
1 elss2prb ⊢ p ∈ e ∈ 𝒫 V | e = 2 ↔ ∃ v ∈ V ∃ w ∈ V v ≠ w ∧ p = v w
2 eleq1 ⊢ p = v w → p ∈ X ↔ v w ∈ X
3 2 adantl ⊢ v ≠ w ∧ p = v w → p ∈ X ↔ v w ∈ X
4 3 biimpcd ⊢ p ∈ X → v ≠ w ∧ p = v w → v w ∈ X
5 4 reximdv ⊢ p ∈ X → ∃ w ∈ V v ≠ w ∧ p = v w → ∃ w ∈ V v w ∈ X
6 5 reximdv ⊢ p ∈ X → ∃ v ∈ V ∃ w ∈ V v ≠ w ∧ p = v w → ∃ v ∈ V ∃ w ∈ V v w ∈ X
7 6 com12 ⊢ ∃ v ∈ V ∃ w ∈ V v ≠ w ∧ p = v w → p ∈ X → ∃ v ∈ V ∃ w ∈ V v w ∈ X
8 1 7 sylbi ⊢ p ∈ e ∈ 𝒫 V | e = 2 → p ∈ X → ∃ v ∈ V ∃ w ∈ V v w ∈ X
9 8 rexlimiv ⊢ ∃ p ∈ e ∈ 𝒫 V | e = 2 p ∈ X → ∃ v ∈ V ∃ w ∈ V v w ∈ X