# Metamath Proof Explorer

## Theorem eqopi

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

Ref Expression
Assertion eqopi ${⊢}\left({A}\in \left({V}×{W}\right)\wedge \left({1}^{st}\left({A}\right)={B}\wedge {2}^{nd}\left({A}\right)={C}\right)\right)\to {A}=⟨{B},{C}⟩$

### Proof

Step Hyp Ref Expression
1 xpss ${⊢}{V}×{W}\subseteq \mathrm{V}×\mathrm{V}$
2 1 sseli ${⊢}{A}\in \left({V}×{W}\right)\to {A}\in \left(\mathrm{V}×\mathrm{V}\right)$
3 elxp6 ${⊢}{A}\in \left(\mathrm{V}×\mathrm{V}\right)↔\left({A}=⟨{1}^{st}\left({A}\right),{2}^{nd}\left({A}\right)⟩\wedge \left({1}^{st}\left({A}\right)\in \mathrm{V}\wedge {2}^{nd}\left({A}\right)\in \mathrm{V}\right)\right)$
4 3 simplbi ${⊢}{A}\in \left(\mathrm{V}×\mathrm{V}\right)\to {A}=⟨{1}^{st}\left({A}\right),{2}^{nd}\left({A}\right)⟩$
5 opeq12 ${⊢}\left({1}^{st}\left({A}\right)={B}\wedge {2}^{nd}\left({A}\right)={C}\right)\to ⟨{1}^{st}\left({A}\right),{2}^{nd}\left({A}\right)⟩=⟨{B},{C}⟩$
6 4 5 sylan9eq ${⊢}\left({A}\in \left(\mathrm{V}×\mathrm{V}\right)\wedge \left({1}^{st}\left({A}\right)={B}\wedge {2}^{nd}\left({A}\right)={C}\right)\right)\to {A}=⟨{B},{C}⟩$
7 2 6 sylan ${⊢}\left({A}\in \left({V}×{W}\right)\wedge \left({1}^{st}\left({A}\right)={B}\wedge {2}^{nd}\left({A}\right)={C}\right)\right)\to {A}=⟨{B},{C}⟩$