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	⊢ ( ∃ 𝑝 ∈ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } 𝑝 ∈ 𝑋 → ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 { 𝑣 , 𝑤 } ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		elss2prb	⊢ ( 𝑝 ∈ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ↔ ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 ( 𝑣 ≠ 𝑤 ∧ 𝑝 = { 𝑣 , 𝑤 } ) )
2		eleq1	⊢ ( 𝑝 = { 𝑣 , 𝑤 } → ( 𝑝 ∈ 𝑋 ↔ { 𝑣 , 𝑤 } ∈ 𝑋 ) )
3	2	adantl	⊢ ( ( 𝑣 ≠ 𝑤 ∧ 𝑝 = { 𝑣 , 𝑤 } ) → ( 𝑝 ∈ 𝑋 ↔ { 𝑣 , 𝑤 } ∈ 𝑋 ) )
4	3	biimpcd	⊢ ( 𝑝 ∈ 𝑋 → ( ( 𝑣 ≠ 𝑤 ∧ 𝑝 = { 𝑣 , 𝑤 } ) → { 𝑣 , 𝑤 } ∈ 𝑋 ) )
5	4	reximdv	⊢ ( 𝑝 ∈ 𝑋 → ( ∃ 𝑤 ∈ 𝑉 ( 𝑣 ≠ 𝑤 ∧ 𝑝 = { 𝑣 , 𝑤 } ) → ∃ 𝑤 ∈ 𝑉 { 𝑣 , 𝑤 } ∈ 𝑋 ) )
6	5	reximdv	⊢ ( 𝑝 ∈ 𝑋 → ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 ( 𝑣 ≠ 𝑤 ∧ 𝑝 = { 𝑣 , 𝑤 } ) → ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 { 𝑣 , 𝑤 } ∈ 𝑋 ) )
7	6	com12	⊢ ( ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 ( 𝑣 ≠ 𝑤 ∧ 𝑝 = { 𝑣 , 𝑤 } ) → ( 𝑝 ∈ 𝑋 → ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 { 𝑣 , 𝑤 } ∈ 𝑋 ) )
8	1 7	sylbi	⊢ ( 𝑝 ∈ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } → ( 𝑝 ∈ 𝑋 → ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 { 𝑣 , 𝑤 } ∈ 𝑋 ) )
9	8	rexlimiv	⊢ ( ∃ 𝑝 ∈ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } 𝑝 ∈ 𝑋 → ∃ 𝑣 ∈ 𝑉 ∃ 𝑤 ∈ 𝑉 { 𝑣 , 𝑤 } ∈ 𝑋 )