Metamath Proof Explorer


Theorem iotacl

Description: Membership law for descriptions.

This can be useful for expanding an unbounded iota-based definition (see df-iota ). If you have a bounded iota-based definition, riotacl2 may be useful.

(Contributed by Andrew Salmon, 1-Aug-2011)

Ref Expression
Assertion iotacl ∃! x φ ι x | φ x | φ

Proof

Step Hyp Ref Expression
1 iota4 ∃! x φ [˙ ι x | φ / x]˙ φ
2 df-sbc [˙ ι x | φ / x]˙ φ ι x | φ x | φ
3 1 2 sylib ∃! x φ ι x | φ x | φ