This is an inofficial mirror of
http://metamath.tirix.org
for personal testing of a visualizer extension only.
Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Restricted iota (description binder)
crio
Next ⟩
df-riota
Metamath Proof Explorer
Unicode
Structured
Syntax definition
crio
Description:
Extend class notation with restricted description binder.
Ref
Expression
Assertion
crio
class ( iota_ x e. A ph )