Theorem otth

Description: Ordered triple theorem. (Contributed by NM, 25-Sep-2014) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypotheses	otth.1	⊢ 𝐴 ∈ V
	otth.2	⊢ 𝐵 ∈ V
	otth.3	⊢ 𝑅 ∈ V
Assertion	otth	⊢ ( ⟨ 𝐴 , 𝐵 , 𝑅 ⟩ = ⟨ 𝐶 , 𝐷 , 𝑆 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		otth.1	⊢ 𝐴 ∈ V
2		otth.2	⊢ 𝐵 ∈ V
3		otth.3	⊢ 𝑅 ∈ V
4		df-ot	⊢ ⟨ 𝐴 , 𝐵 , 𝑅 ⟩ = ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑅 ⟩
5		df-ot	⊢ ⟨ 𝐶 , 𝐷 , 𝑆 ⟩ = ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑆 ⟩
6	4 5	eqeq12i	⊢ ( ⟨ 𝐴 , 𝐵 , 𝑅 ⟩ = ⟨ 𝐶 , 𝐷 , 𝑆 ⟩ ↔ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑅 ⟩ = ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑆 ⟩ )
7	1 2 3	otth2	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝑅 ⟩ = ⟨ ⟨ 𝐶 , 𝐷 ⟩ , 𝑆 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆 ) )
8	6 7	bitri	⊢ ( ⟨ 𝐴 , 𝐵 , 𝑅 ⟩ = ⟨ 𝐶 , 𝐷 , 𝑆 ⟩ ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ∧ 𝑅 = 𝑆 ) )