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 ((A \in V \land B \in V \land C \in V) \leftrightarrow (R \in V \land S \in V \land T \in V))$

Proof

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