Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Restricted quantification
wreu
Next ⟩
wrmo
Metamath Proof Explorer
Ascii
Unicode
Syntax definition
wreu
Description:
Extend wff notation to include restricted existential uniqueness.
Ref
Expression
Assertion
wreu
$${wff}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi}$$