NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-opk Structured version   GIF version

Definition df-opk 4058
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 4566, 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
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2copk 4057 . 2 class A, B
41csn 3737 . . 3 class {A}
51, 2cpr 3738 . . 3 class {A, B}
64, 5cpr 3738 . 2 class {{A}, {A, B}}
73, 6wceq 1642 1 wff A, B⟫ = {{A}, {A, B}}
Colors of variables: wff set class
This definition is referenced by:  opkeq1  4059  opkeq2  4060  nfopk  4068  axprimlem2  4089  opkex  4113  elopk  4129  opkthg  4131
  Copyright terms: Public domain W3C validator