Theorem eqop2

Description: Two ways to express equality with an ordered pair. (Contributed by NM, 25-Feb-2014)

	Ref	Expression
Hypotheses	eqop2.1	⊢ 𝐵 ∈ V
	eqop2.2	⊢ 𝐶 ∈ V
Assertion	eqop2	⊢ ( 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝐴 ) = 𝐵 ∧ ( 2nd ‘ 𝐴 ) = 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqop2.1	⊢ 𝐵 ∈ V
2		eqop2.2	⊢ 𝐶 ∈ V
3	1 2	opelvv	⊢ ⟨ 𝐵 , 𝐶 ⟩ ∈ ( V × V )
4		eleq1	⊢ ( 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ → ( 𝐴 ∈ ( V × V ) ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ ( V × V ) ) )
5	3 4	mpbiri	⊢ ( 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ → 𝐴 ∈ ( V × V ) )
6		eqop	⊢ ( 𝐴 ∈ ( V × V ) → ( 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ ↔ ( ( 1st ‘ 𝐴 ) = 𝐵 ∧ ( 2nd ‘ 𝐴 ) = 𝐶 ) ) )
7	5 6	biadanii	⊢ ( 𝐴 = ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝐴 ) = 𝐵 ∧ ( 2nd ‘ 𝐴 ) = 𝐶 ) ) )