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

Metamath Proof Explorer

Theorem oteqex

Description: Equivalence of existence implied by equality of ordered triples. (Contributed by NM, 28-May-2008) (Revised by Mario Carneiro, 26-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 simp3 ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → 𝐶 ∈ V )
2 1 a1i ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) → 𝐶 ∈ V ) )
3 simp3 ⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ∧ 𝑇 ∈ V ) → 𝑇 ∈ V )
4 oteqex2 ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ → ( 𝐶 ∈ V ↔ 𝑇 ∈ V ) )
5 3 4 imbitrrid ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ → ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ∧ 𝑇 ∈ V ) → 𝐶 ∈ V ) )
6 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
7 opthg ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ V ∧ 𝐶 ∈ V ) → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑅 , 𝑆 ⟩ ∧ 𝐶 = 𝑇 ) ) )
8 6 7 mpan ⊢ ( 𝐶 ∈ V → ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ ↔ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑅 , 𝑆 ⟩ ∧ 𝐶 = 𝑇 ) ) )
9 8 simprbda ⊢ ( ( 𝐶 ∈ V ∧ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ ) → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑅 , 𝑆 ⟩ )
10 opeqex ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑅 , 𝑆 ⟩ → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ) )
11 9 10 syl ⊢ ( ( 𝐶 ∈ V ∧ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ ) → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ) )
12 4 adantl ⊢ ( ( 𝐶 ∈ V ∧ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ ) → ( 𝐶 ∈ V ↔ 𝑇 ∈ V ) )
13 11 12 anbi12d ⊢ ( ( 𝐶 ∈ V ∧ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ ) → ( ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐶 ∈ V ) ↔ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ 𝑇 ∈ V ) ) )
14 df-3an ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝐶 ∈ V ) )
15 df-3an ⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ∧ 𝑇 ∈ V ) ↔ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) ∧ 𝑇 ∈ V ) )
16 13 14 15 3bitr4g ⊢ ( ( 𝐶 ∈ V ∧ ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ ) → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ↔ ( 𝑅 ∈ V ∧ 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) )
17 16 expcom ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ → ( 𝐶 ∈ V → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ↔ ( 𝑅 ∈ V ∧ 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) ) )
18 2 5 17 pm5.21ndd ⊢ ( ⟨ ⟨ 𝐴 , 𝐵 ⟩ , 𝐶 ⟩ = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , 𝑇 ⟩ → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐶 ∈ V ) ↔ ( 𝑅 ∈ V ∧ 𝑆 ∈ V ∧ 𝑇 ∈ V ) ) )