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 ) ) )