oteqex2

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

		Ref	Expression
	Assertion	oteqex2	$⊢ ⟨⟨A, B⟩, C⟩ = ⟨⟨R, S⟩, T⟩ \to (C \in V \leftrightarrow T \in V)$

Step	Hyp	Ref	Expression
1		opeqex	$⊢ ⟨⟨A, B⟩, C⟩ = ⟨⟨R, S⟩, T⟩ \to ((⟨A, B⟩ \in V \land C \in V) \leftrightarrow (⟨R, S⟩ \in V \land T \in V))$
2		opex	$⊢ ⟨A, B⟩ \in V$
3	2	biantrur	$⊢ C \in V \leftrightarrow (⟨A, B⟩ \in V \land C \in V)$
4		opex	$⊢ ⟨R, S⟩ \in V$
5	4	biantrur	$⊢ T \in V \leftrightarrow (⟨R, S⟩ \in V \land T \in V)$
6	1 3 5	3bitr4g	$⊢ ⟨⟨A, B⟩, C⟩ = ⟨⟨R, S⟩, T⟩ \to (C \in V \leftrightarrow T \in V)$

Metamath Proof Explorer