# Metamath Proof Explorer

## Theorem opthg

Description: Ordered pair theorem. C and D are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005) (Revised by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion opthg ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(⟨{A},{B}⟩=⟨{C},{D}⟩↔\left({A}={C}\wedge {B}={D}\right)\right)$

### Proof

Step Hyp Ref Expression
1 opeq1 ${⊢}{x}={A}\to ⟨{x},{y}⟩=⟨{A},{y}⟩$
2 1 eqeq1d ${⊢}{x}={A}\to \left(⟨{x},{y}⟩=⟨{C},{D}⟩↔⟨{A},{y}⟩=⟨{C},{D}⟩\right)$
3 eqeq1 ${⊢}{x}={A}\to \left({x}={C}↔{A}={C}\right)$
4 3 anbi1d ${⊢}{x}={A}\to \left(\left({x}={C}\wedge {y}={D}\right)↔\left({A}={C}\wedge {y}={D}\right)\right)$
5 2 4 bibi12d ${⊢}{x}={A}\to \left(\left(⟨{x},{y}⟩=⟨{C},{D}⟩↔\left({x}={C}\wedge {y}={D}\right)\right)↔\left(⟨{A},{y}⟩=⟨{C},{D}⟩↔\left({A}={C}\wedge {y}={D}\right)\right)\right)$
6 opeq2 ${⊢}{y}={B}\to ⟨{A},{y}⟩=⟨{A},{B}⟩$
7 6 eqeq1d ${⊢}{y}={B}\to \left(⟨{A},{y}⟩=⟨{C},{D}⟩↔⟨{A},{B}⟩=⟨{C},{D}⟩\right)$
8 eqeq1 ${⊢}{y}={B}\to \left({y}={D}↔{B}={D}\right)$
9 8 anbi2d ${⊢}{y}={B}\to \left(\left({A}={C}\wedge {y}={D}\right)↔\left({A}={C}\wedge {B}={D}\right)\right)$
10 7 9 bibi12d ${⊢}{y}={B}\to \left(\left(⟨{A},{y}⟩=⟨{C},{D}⟩↔\left({A}={C}\wedge {y}={D}\right)\right)↔\left(⟨{A},{B}⟩=⟨{C},{D}⟩↔\left({A}={C}\wedge {B}={D}\right)\right)\right)$
11 vex ${⊢}{x}\in \mathrm{V}$
12 vex ${⊢}{y}\in \mathrm{V}$
13 11 12 opth ${⊢}⟨{x},{y}⟩=⟨{C},{D}⟩↔\left({x}={C}\wedge {y}={D}\right)$
14 5 10 13 vtocl2g ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(⟨{A},{B}⟩=⟨{C},{D}⟩↔\left({A}={C}\wedge {B}={D}\right)\right)$