Metamath Proof Explorer

Theorem 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 → C ∈ V ↔ T ∈ V

Proof

Step Hyp Ref Expression
1 opeqex ⊢ A B C = R S T → A B ∈ V ∧ C ∈ V ↔ R S ∈ V ∧ T ∈ V
2 opex ⊢ A B ∈ V
3 2 biantrur ⊢ C ∈ V ↔ A B ∈ V ∧ C ∈ V
4 opex ⊢ R S ∈ V
5 4 biantrur ⊢ T ∈ V ↔ R S ∈ V ∧ T ∈ V
6 1 3 5 3bitr4g ⊢ A B C = R S T → C ∈ V ↔ T ∈ V