Definition df-opk 4059

Description: Define the Kuratowski ordered pair. This ordered pair definition is standard for ZFC set theory, but we do not use it beyond establishing df-op 4567, since it is not type-level. We state this definition since it is a simple definition that can be used by the set construction axioms that follow this section. (Contributed by SF, 12-Jan-2015.)

Assertion

Ref	Expression
df-opk	⊢ ⟪A, B⟫ = {{A}, {A, B}}

Detailed syntax breakdown of Definition df-opk

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	copk 4058	. 2 class ⟪A, B⟫
4	1	csn 3738	. . 3 class {A}
5	1, 2	cpr 3739	. . 3 class {A, B}
6	4, 5	cpr 3739	. 2 class {{A}, {A, B}}
7	3, 6	wceq 1642	1 wff ⟪A, B⟫ = {{A}, {A, B}}

This definition is referenced by:  opkeq1  4060  opkeq2  4061  nfopk  4069  axprimlem2  4090  opkex  4114  elopk  4130  opkthg  4132