Theorem oteqex2

Description: Equivalence of existence implied by equality of ordered triples. (Contributed by NM, 26-Apr-2015)

	Ref	Expression
Assertion	oteqex2	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ → ( 𝐶 ∈ V ↔ 𝑇 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		opeqex	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ → ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ V ∧ 𝐶 ∈ V ) ↔ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ V ∧ 𝑇 ∈ V ) ) )
2		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
3	2	biantrur	⊢ ( 𝐶 ∈ V ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ V ∧ 𝐶 ∈ V ) )
4		opex	⊢ ⟨ 𝑅 , 𝑆 ⟩ ∈ V
5	4	biantrur	⊢ ( 𝑇 ∈ V ↔ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ V ∧ 𝑇 ∈ V ) )
6	1 3 5	3bitr4g	⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ → ( 𝐶 ∈ V ↔ 𝑇 ∈ V ) )