Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Restricted iota (description binder)
riota1a
Next ⟩
riota2df
Metamath Proof Explorer
Ascii
Unicode
Theorem
riota1a
Description:
Property of iota.
(Contributed by
NM
, 23-Aug-2011)
Ref
Expression
Assertion
riota1a
⊢
x
∈
A
∧
∃!
x
∈
A
φ
→
φ
↔
ι
x
|
x
∈
A
∧
φ
=
x
Proof
Step
Hyp
Ref
Expression
1
ibar
⊢
x
∈
A
→
φ
↔
x
∈
A
∧
φ
2
df-reu
⊢
∃!
x
∈
A
φ
↔
∃!
x
x
∈
A
∧
φ
3
iota1
⊢
∃!
x
x
∈
A
∧
φ
→
x
∈
A
∧
φ
↔
ι
x
|
x
∈
A
∧
φ
=
x
4
2
3
sylbi
⊢
∃!
x
∈
A
φ
→
x
∈
A
∧
φ
↔
ι
x
|
x
∈
A
∧
φ
=
x
5
1
4
sylan9bb
⊢
x
∈
A
∧
∃!
x
∈
A
φ
→
φ
↔
ι
x
|
x
∈
A
∧
φ
=
x