Theorem 1st2ndb

Description: Reconstruction of an ordered pair in terms of its components. (Contributed by NM, 25-Feb-2014)

	Ref	Expression
Assertion	1st2ndb	⊢ ( 𝐴 ∈ ( V × V ) ↔ 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		1st2nd2	⊢ ( 𝐴 ∈ ( V × V ) → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
2		id	⊢ ( 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ → 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )
3		fvex	⊢ ( 1st ‘ 𝐴 ) ∈ V
4		fvex	⊢ ( 2nd ‘ 𝐴 ) ∈ V
5	3 4	opelvv	⊢ ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ ∈ ( V × V )
6	2 5	eqeltrdi	⊢ ( 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ → 𝐴 ∈ ( V × V ) )
7	1 6	impbii	⊢ ( 𝐴 ∈ ( V × V ) ↔ 𝐴 = ⟨ ( 1st ‘ 𝐴 ) , ( 2nd ‘ 𝐴 ) ⟩ )