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

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	⊢ 𝐵 ∈ V
	elop.2	⊢ 𝐶 ∈ V
Assertion	elop	⊢ ( 𝐴 ∈ ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 = { 𝐵 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) )

Proof

Step	Hyp	Ref	Expression
1		elop.1	⊢ 𝐵 ∈ V
2		elop.2	⊢ 𝐶 ∈ V
3		elopg	⊢ ( ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐴 ∈ ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 = { 𝐵 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) ) )
4	1 2 3	mp2an	⊢ ( 𝐴 ∈ ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 = { 𝐵 } ∨ 𝐴 = { 𝐵 , 𝐶 } ) )