Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Ordered-pair class abstractions (class builders)
copab
Next ⟩
df-opab
Metamath Proof Explorer
Ascii
Structured
Syntax definition
copab
Description:
Extend class notation to include ordered-pair class abstraction (class builder).
Ref
Expression
Assertion
copab
class
{ 〈
𝑥
,
𝑦
〉 ∣
𝜑
}