Theorem altopex

Description: Alternative ordered pairs always exist. (Contributed by Scott Fenton, 22-Mar-2012)

	Ref	Expression
Assertion	altopex	⊢ ⟪ 𝐴 , 𝐵 ⟫ ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-altop	⊢ ⟪ 𝐴 , 𝐵 ⟫ = { { 𝐴 } , { 𝐴 , { 𝐵 } } }
2		prex	⊢ { { 𝐴 } , { 𝐴 , { 𝐵 } } } ∈ V
3	1 2	eqeltri	⊢ ⟪ 𝐴 , 𝐵 ⟫ ∈ V