Theorem altopex

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

	Ref	Expression
Assertion	altopex	$$⊢⟪A,B⟫\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-altop	$$⊢⟪A,B⟫=\left\{\left\{A\right\},\left\{A,\left\{B\right\}\right\}\right\}$$
2		prex	$$⊢\left\{\left\{A\right\},\left\{A,\left\{B\right\}\right\}\right\}\in \mathrm{V}$$
3	1 2	eqeltri	$$⊢⟪A,B⟫\in \mathrm{V}$$