Metamath Proof Explorer


Theorem iota2

Description: The unique element such that ph . (Contributed by Jeff Madsen, 1-Jun-2011) (Revised by Mario Carneiro, 23-Dec-2016)

Ref Expression
Hypothesis iota2.1 x=Aφψ
Assertion iota2 AB∃!xφψιx|φ=A

Proof

Step Hyp Ref Expression
1 iota2.1 x=Aφψ
2 elex ABAV
3 simpl AV∃!xφAV
4 simpr AV∃!xφ∃!xφ
5 1 adantl AV∃!xφx=Aφψ
6 nfv xAV
7 nfeu1 x∃!xφ
8 6 7 nfan xAV∃!xφ
9 nfvd AV∃!xφxψ
10 nfcvd AV∃!xφ_xA
11 3 4 5 8 9 10 iota2df AV∃!xφψιx|φ=A
12 2 11 sylan AB∃!xφψιx|φ=A