This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 → A ∈ V ∧ B ∈ V ∧ C ∈ V ↔ R ∈ V ∧ S ∈ V ∧ T ∈ V

Proof

Step Hyp Ref Expression
1 simp3 ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V → C ∈ V
2 1 a1i ⊢ A B C = R S T → A ∈ V ∧ B ∈ V ∧ C ∈ V → C ∈ V
3 simp3 ⊢ R ∈ V ∧ S ∈ V ∧ T ∈ V → T ∈ V
4 oteqex2 ⊢ A B C = R S T → C ∈ V ↔ T ∈ V
5 3 4 imbitrrid ⊢ A B C = R S T → R ∈ V ∧ S ∈ V ∧ T ∈ V → C ∈ V
6 opex ⊢ A B ∈ V
7 opthg ⊢ A B ∈ V ∧ C ∈ V → A B C = R S T ↔ A B = R S ∧ C = T
8 6 7 mpan ⊢ C ∈ V → A B C = R S T ↔ A B = R S ∧ C = T
9 8 simprbda ⊢ C ∈ V ∧ A B C = R S T → A B = R S
10 opeqex ⊢ A B = R S → A ∈ V ∧ B ∈ V ↔ R ∈ V ∧ S ∈ V
11 9 10 syl ⊢ C ∈ V ∧ A B C = R S T → A ∈ V ∧ B ∈ V ↔ R ∈ V ∧ S ∈ V
12 4 adantl ⊢ C ∈ V ∧ A B C = R S T → C ∈ V ↔ T ∈ V
13 11 12 anbi12d ⊢ C ∈ V ∧ A B C = R S T → A ∈ V ∧ B ∈ V ∧ C ∈ V ↔ R ∈ V ∧ S ∈ V ∧ T ∈ V
14 df-3an ⊢ A ∈ V ∧ B ∈ V ∧ C ∈ V ↔ A ∈ V ∧ B ∈ V ∧ C ∈ V
15 df-3an ⊢ R ∈ V ∧ S ∈ V ∧ T ∈ V ↔ R ∈ V ∧ S ∈ V ∧ T ∈ V
16 13 14 15 3bitr4g ⊢ C ∈ V ∧ A B C = R S T → A ∈ V ∧ B ∈ V ∧ C ∈ V ↔ R ∈ V ∧ S ∈ V ∧ T ∈ V
17 16 expcom ⊢ A B C = R S T → C ∈ V → A ∈ V ∧ B ∈ V ∧ C ∈ V ↔ R ∈ V ∧ S ∈ V ∧ T ∈ V
18 2 5 17 pm5.21ndd ⊢ A B C = R S T → A ∈ V ∧ B ∈ V ∧ C ∈ V ↔ R ∈ V ∧ S ∈ V ∧ T ∈ V