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 >> = { { A } , { A , { B } } }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	caltop	|- << A , B >>
3	0	csn	|- { A }
4	1	csn	|- { B }
5	0 4	cpr	|- { A , { B } }
6	3 5	cpr	|- { { A } , { A , { B } } }
7	2 6	wceq	|- << A , B >> = { { A } , { A , { B } } }