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 ${⊢}⟨⟨{A},{B}⟩,{C}⟩=⟨⟨{R},{S}⟩,{T}⟩\to \left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)↔\left({R}\in \mathrm{V}\wedge {S}\in \mathrm{V}\wedge {T}\in \mathrm{V}\right)\right)$

Proof

Step Hyp Ref Expression
1 simp3 ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)\to {C}\in \mathrm{V}$
2 1 a1i ${⊢}⟨⟨{A},{B}⟩,{C}⟩=⟨⟨{R},{S}⟩,{T}⟩\to \left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)\to {C}\in \mathrm{V}\right)$
3 simp3 ${⊢}\left({R}\in \mathrm{V}\wedge {S}\in \mathrm{V}\wedge {T}\in \mathrm{V}\right)\to {T}\in \mathrm{V}$
4 oteqex2 ${⊢}⟨⟨{A},{B}⟩,{C}⟩=⟨⟨{R},{S}⟩,{T}⟩\to \left({C}\in \mathrm{V}↔{T}\in \mathrm{V}\right)$
5 3 4 syl5ibr ${⊢}⟨⟨{A},{B}⟩,{C}⟩=⟨⟨{R},{S}⟩,{T}⟩\to \left(\left({R}\in \mathrm{V}\wedge {S}\in \mathrm{V}\wedge {T}\in \mathrm{V}\right)\to {C}\in \mathrm{V}\right)$
6 opex ${⊢}⟨{A},{B}⟩\in \mathrm{V}$
7 opthg ${⊢}\left(⟨{A},{B}⟩\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)\to \left(⟨⟨{A},{B}⟩,{C}⟩=⟨⟨{R},{S}⟩,{T}⟩↔\left(⟨{A},{B}⟩=⟨{R},{S}⟩\wedge {C}={T}\right)\right)$
8 6 7 mpan ${⊢}{C}\in \mathrm{V}\to \left(⟨⟨{A},{B}⟩,{C}⟩=⟨⟨{R},{S}⟩,{T}⟩↔\left(⟨{A},{B}⟩=⟨{R},{S}⟩\wedge {C}={T}\right)\right)$
9 8 simprbda ${⊢}\left({C}\in \mathrm{V}\wedge ⟨⟨{A},{B}⟩,{C}⟩=⟨⟨{R},{S}⟩,{T}⟩\right)\to ⟨{A},{B}⟩=⟨{R},{S}⟩$
10 opeqex ${⊢}⟨{A},{B}⟩=⟨{R},{S}⟩\to \left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)↔\left({R}\in \mathrm{V}\wedge {S}\in \mathrm{V}\right)\right)$
11 9 10 syl ${⊢}\left({C}\in \mathrm{V}\wedge ⟨⟨{A},{B}⟩,{C}⟩=⟨⟨{R},{S}⟩,{T}⟩\right)\to \left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)↔\left({R}\in \mathrm{V}\wedge {S}\in \mathrm{V}\right)\right)$
12 4 adantl ${⊢}\left({C}\in \mathrm{V}\wedge ⟨⟨{A},{B}⟩,{C}⟩=⟨⟨{R},{S}⟩,{T}⟩\right)\to \left({C}\in \mathrm{V}↔{T}\in \mathrm{V}\right)$
13 11 12 anbi12d ${⊢}\left({C}\in \mathrm{V}\wedge ⟨⟨{A},{B}⟩,{C}⟩=⟨⟨{R},{S}⟩,{T}⟩\right)\to \left(\left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\wedge {C}\in \mathrm{V}\right)↔\left(\left({R}\in \mathrm{V}\wedge {S}\in \mathrm{V}\right)\wedge {T}\in \mathrm{V}\right)\right)$
14 df-3an ${⊢}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)↔\left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)\wedge {C}\in \mathrm{V}\right)$
15 df-3an ${⊢}\left({R}\in \mathrm{V}\wedge {S}\in \mathrm{V}\wedge {T}\in \mathrm{V}\right)↔\left(\left({R}\in \mathrm{V}\wedge {S}\in \mathrm{V}\right)\wedge {T}\in \mathrm{V}\right)$
16 13 14 15 3bitr4g ${⊢}\left({C}\in \mathrm{V}\wedge ⟨⟨{A},{B}⟩,{C}⟩=⟨⟨{R},{S}⟩,{T}⟩\right)\to \left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)↔\left({R}\in \mathrm{V}\wedge {S}\in \mathrm{V}\wedge {T}\in \mathrm{V}\right)\right)$
17 16 expcom ${⊢}⟨⟨{A},{B}⟩,{C}⟩=⟨⟨{R},{S}⟩,{T}⟩\to \left({C}\in \mathrm{V}\to \left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)↔\left({R}\in \mathrm{V}\wedge {S}\in \mathrm{V}\wedge {T}\in \mathrm{V}\right)\right)\right)$
18 2 5 17 pm5.21ndd ${⊢}⟨⟨{A},{B}⟩,{C}⟩=⟨⟨{R},{S}⟩,{T}⟩\to \left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\wedge {C}\in \mathrm{V}\right)↔\left({R}\in \mathrm{V}\wedge {S}\in \mathrm{V}\wedge {T}\in \mathrm{V}\right)\right)$