Definition df-altop 31235

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

Assertion

Ref	Expression
df-altop	⊢ ⟪𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}

Detailed syntax breakdown of Definition df-altop

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	caltop 31233	. 2 class ⟪𝐴, 𝐵⟫
4	1	csn 4125	. . 3 class {𝐴}
5	2	csn 4125	. . . 4 class {𝐵}
6	1, 5	cpr 4127	. . 3 class {𝐴, {𝐵}}
7	4, 6	cpr 4127	. 2 class {{𝐴}, {𝐴, {𝐵}}}
8	3, 7	wceq 1475	1 wff ⟪𝐴, 𝐵⟫ = {{𝐴}, {𝐴, {𝐵}}}

This definition is referenced by:  altopex  31237  altopthsn  31238  altxpsspw  31254  rankaltopb  31256  nfaltop  31257