Metamath Proof Explorer

Theorem elop

Description: Characterization of the elements of an ordered pair. Exercise 3 of TakeutiZaring p. 15. (Contributed by NM, 15-Jul-1993) (Revised by Mario Carneiro, 26-Apr-2015) Remove an extraneous hypothesis. (Revised by BJ, 25-Dec-2020) (Avoid depending on this detail.)

Ref Expression
Hypotheses elop.1 ⊢ B ∈ V
elop.2 ⊢ C ∈ V
Assertion elop ⊢ A ∈ B C ↔ A = B ∨ A = B C

Proof

Step Hyp Ref Expression
1 elop.1 ⊢ B ∈ V
2 elop.2 ⊢ C ∈ V
3 elopg ⊢ B ∈ V ∧ C ∈ V → A ∈ B C ↔ A = B ∨ A = B C
4 1 2 3 mp2an ⊢ A ∈ B C ↔ A = B ∨ A = B C