eqop

Description: Two ways to express equality with an ordered pair. (Contributed by NM, 3-Sep-2007) (Proof shortened by Mario Carneiro, 26-Apr-2015)

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

Step	Hyp	Ref	Expression
1		1st2nd2	⊢ ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ )
2	1	eqeq1d	⊢ ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → ( 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) )
3		fvex	⊢ ( 1^st ‘ 𝐴 ) ∈ V
4		fvex	⊢ ( 2^nd ‘ 𝐴 ) ∈ V
5	3 4	opth	⊢ ( ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ↔ ( ( 1^st ‘ 𝐴 ) = 𝐵 ∧ ( 2^nd ‘ 𝐴 ) = 𝐶 ) )
6	2 5	bitrdi	⊢ ( 𝐴 ∈ ( 𝑉 × 𝑊 ) → ( 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ ↔ ( ( 1^st ‘ 𝐴 ) = 𝐵 ∧ ( 2^nd ‘ 𝐴 ) = 𝐶 ) ) )

Metamath Proof Explorer