Metamath Proof Explorer


Theorem iotan0

Description: Representation of "the unique element such that ph " with a class expression A which is not the empty set (that means that "the unique element such that ph " exists). (Contributed by AV, 30-Jan-2024)

Ref Expression
Hypothesis iotan0.1 x=Aφψ
Assertion iotan0 AVAA=ιx|φψ

Proof

Step Hyp Ref Expression
1 iotan0.1 x=Aφψ
2 pm13.18 A=ιx|φAιx|φ
3 2 expcom AA=ιx|φιx|φ
4 iotanul ¬∃!xφιx|φ=
5 4 necon1ai ιx|φ∃!xφ
6 3 5 syl6 AA=ιx|φ∃!xφ
7 6 a1i AVAA=ιx|φ∃!xφ
8 7 3imp AVAA=ιx|φ∃!xφ
9 eqcom A=ιx|φιx|φ=A
10 1 iota2 AV∃!xφψιx|φ=A
11 10 biimprd AV∃!xφιx|φ=Aψ
12 9 11 biimtrid AV∃!xφA=ιx|φψ
13 12 impancom AVA=ιx|φ∃!xφψ
14 13 3adant2 AVAA=ιx|φ∃!xφψ
15 8 14 mpd AVAA=ιx|φψ