eqopi

Description: Equality with an ordered pair. (Contributed by NM, 15-Dec-2008) (Revised by Mario Carneiro, 23-Feb-2014)

		Ref	Expression
	Assertion	eqopi	⊢ ( ( 𝐴 ∈ ( 𝑉 × 𝑊 ) ∧ ( ( 1^st ‘ 𝐴 ) = 𝐵 ∧ ( 2^nd ‘ 𝐴 ) = 𝐶 ) ) → 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ )

Step	Hyp	Ref	Expression
1		xpss	⊢ ( 𝑉 × 𝑊 ) ⊆ ( V × V )
2	1	sseli	⊢ ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → 𝐴 ∈ ( V × V ) )
3		elxp6	⊢ ( 𝐴 ∈ ( V × V ) ↔ ( 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ∧ ( ( 1^st ‘ 𝐴 ) ∈ V ∧ ( 2^nd ‘ 𝐴 ) ∈ V ) ) )
4	3	simplbi	⊢ ( 𝐴 ∈ ( V × V ) → 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ )
5		opeq12	⊢ ( ( ( 1^st ‘ 𝐴 ) = 𝐵 ∧ ( 2^nd ‘ 𝐴 ) = 𝐶 ) → ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ = ⟨ 𝐵 , 𝐶 ⟩ )
6	4 5	sylan9eq	⊢ ( ( 𝐴 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝐴 ) = 𝐵 ∧ ( 2^nd ‘ 𝐴 ) = 𝐶 ) ) → 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ )
7	2 6	sylan	⊢ ( ( 𝐴 ∈ ( 𝑉 × 𝑊 ) ∧ ( ( 1^st ‘ 𝐴 ) = 𝐵 ∧ ( 2^nd ‘ 𝐴 ) = 𝐶 ) ) → 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ )

Metamath Proof Explorer