This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		opeq1	⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
2	1	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ) )
3		eqeq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 = 𝐶 ↔ 𝐴 = 𝐶 ) )
4	3	anbi1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ↔ ( 𝐴 = 𝐶 ∧ 𝑦 = 𝐷 ) ) )
5	2 4	bibi12d	⊢ ( 𝑥 = 𝐴 → ( ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ↔ ( ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ) )
6		opeq2	⊢ ( 𝑦 = 𝐵 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
7	6	eqeq1d	⊢ ( 𝑦 = 𝐵 → ( ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ) )
8		eqeq1	⊢ ( 𝑦 = 𝐵 → ( 𝑦 = 𝐷 ↔ 𝐵 = 𝐷 ) )
9	8	anbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 = 𝐶 ∧ 𝑦 = 𝐷 ) ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )
10	7 9	bibi12d	⊢ ( 𝑦 = 𝐵 → ( ( ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝑦 = 𝐷 ) ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) ) )
11		vex	⊢ 𝑥 ∈ V
12		vex	⊢ 𝑦 ∈ V
13	11 12	opth	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝑥 = 𝐶 ∧ 𝑦 = 𝐷 ) )
14	5 10 13	vtocl2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )