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=2p∈X→∃v∈V∃w∈Vvw∈X

Proof

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