Theorem opi2

Description: One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993) (Revised by Mario Carneiro, 26-Apr-2015) (Avoid depending on this detail.)

	Ref	Expression
Hypotheses	opi1.1	⊢ 𝐴 ∈ V
	opi1.2	⊢ 𝐵 ∈ V
Assertion	opi2	⊢ { 𝐴 , 𝐵 } ∈ ⟨ 𝐴 , 𝐵 ⟩

Proof

Step	Hyp	Ref	Expression
1		opi1.1	⊢ 𝐴 ∈ V
2		opi1.2	⊢ 𝐵 ∈ V
3		prex	⊢ { 𝐴 , 𝐵 } ∈ V
4	3	prid2	⊢ { 𝐴 , 𝐵 } ∈ { { 𝐴 } , { 𝐴 , 𝐵 } }
5	1 2	dfop	⊢ ⟨ 𝐴 , 𝐵 ⟩ = { { 𝐴 } , { 𝐴 , 𝐵 } }
6	4 5	eleqtrri	⊢ { 𝐴 , 𝐵 } ∈ ⟨ 𝐴 , 𝐵 ⟩