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

Metamath Proof Explorer

Theorem xpopth

Description: An ordered pair theorem for members of Cartesian products. (Contributed by NM, 20-Jun-2007)

Ref Expression
Assertion xpopth ⊢ A ∈ C × D ∧ B ∈ R × S → 1 st ⁡ A = 1 st ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B ↔ A = B

Proof

Step Hyp Ref Expression
1 1st2nd2 ⊢ A ∈ C × D → A = 1 st ⁡ A 2 nd ⁡ A
2 1st2nd2 ⊢ B ∈ R × S → B = 1 st ⁡ B 2 nd ⁡ B
3 1 2 eqeqan12d ⊢ A ∈ C × D ∧ B ∈ R × S → A = B ↔ 1 st ⁡ A 2 nd ⁡ A = 1 st ⁡ B 2 nd ⁡ B
4 fvex ⊢ 1 st ⁡ A ∈ V
5 fvex ⊢ 2 nd ⁡ A ∈ V
6 4 5 opth ⊢ 1 st ⁡ A 2 nd ⁡ A = 1 st ⁡ B 2 nd ⁡ B ↔ 1 st ⁡ A = 1 st ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B
7 3 6 bitr2di ⊢ A ∈ C × D ∧ B ∈ R × S → 1 st ⁡ A = 1 st ⁡ B ∧ 2 nd ⁡ A = 2 nd ⁡ B ↔ A = B