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

Definition df-opk 2863
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 3674, 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.
Assertion
Ref Expression
df-opk

Detailed syntax breakdown of Definition df-opk
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2copk 2862 . 2
41csn 2803 . . 3
51, 2cpr 2804 . . 3
64, 5cpr 2804 . 2
73, 6wceq 1398 1
Colors of variables: wff set class
This definition is referenced by:  opkeq1  2864  opkeq2  2865  hbopk  2873  axprimlem2  3191  opkex  3215  elopk  3233  opkthg  3235
  Copyright terms: Public domain W3C validator