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

Metamath Proof Explorer

Theorem opeqex

Description: Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008)

Ref Expression
Assertion opeqex ⊢ A B = C D → A ∈ V ∧ B ∈ V ↔ C ∈ V ∧ D ∈ V

Proof

Step Hyp Ref Expression
1 neeq1 ⊢ A B = C D → A B ≠ ∅ ↔ C D ≠ ∅
2 opnz ⊢ A B ≠ ∅ ↔ A ∈ V ∧ B ∈ V
3 opnz ⊢ C D ≠ ∅ ↔ C ∈ V ∧ D ∈ V
4 1 2 3 3bitr3g ⊢ A B = C D → A ∈ V ∧ B ∈ V ↔ C ∈ V ∧ D ∈ V