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

Metamath Proof Explorer

Theorem elopg

Description: Characterization of the elements of an ordered pair. Closed form of elop . (Contributed by BJ, 22-Jun-2019) (Avoid depending on this detail.)

Ref Expression
Assertion elopg ⊢ A ∈ V ∧ B ∈ W → C ∈ A B ↔ C = A ∨ C = A B

Proof

Step Hyp Ref Expression
1 dfopg ⊢ A ∈ V ∧ B ∈ W → A B = A A B
2 eleq2 ⊢ A B = A A B → C ∈ A B ↔ C ∈ A A B
3 snex ⊢ A ∈ V
4 prex ⊢ A B ∈ V
5 3 4 elpr2 ⊢ C ∈ A A B ↔ C = A ∨ C = A B
6 2 5 bitrdi ⊢ A B = A A B → C ∈ A B ↔ C = A ∨ C = A B
7 1 6 syl ⊢ A ∈ V ∧ B ∈ W → C ∈ A B ↔ C = A ∨ C = A B