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	⊢ ⟪ 𝐴 , 𝐵 ⟫ = { { 𝐴 } , { 𝐴 , { 𝐵 } } }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	caltop	⊢ ⟪ 𝐴 , 𝐵 ⟫
3	0	csn	⊢ { 𝐴 }
4	1	csn	⊢ { 𝐵 }
5	0 4	cpr	⊢ { 𝐴 , { 𝐵 } }
6	3 5	cpr	⊢ { { 𝐴 } , { 𝐴 , { 𝐵 } } }
7	2 6	wceq	⊢ ⟪ 𝐴 , 𝐵 ⟫ = { { 𝐴 } , { 𝐴 , { 𝐵 } } }