Definition df-altop

Description: An alternative definition of ordered pairs. This definition removes a hypothesis from its defining theorem (see altopth ), making it more convenient in some circumstances. (Contributed by Scott Fenton, 22-Mar-2012)

	Ref	Expression
Assertion	df-altop	$$⊢⟪A,B⟫=\left\{\left\{A\right\},\left\{A,\left\{B\right\}\right\}\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	caltop	$$class⟪A,B⟫$$
3	0	csn	$$class\left\{A\right\}$$
4	1	csn	$$class\left\{B\right\}$$
5	0 4	cpr	$$class\left\{A,\left\{B\right\}\right\}$$
6	3 5	cpr	$$class\left\{\left\{A\right\},\left\{A,\left\{B\right\}\right\}\right\}$$
7	2 6	wceq	$$wff⟪A,B⟫=\left\{\left\{A\right\},\left\{A,\left\{B\right\}\right\}\right\}$$