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 | |
|
Assertion | iotan0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iotan0.1 | |
|
2 | pm13.18 | |
|
3 | 2 | expcom | |
4 | iotanul | |
|
5 | 4 | necon1ai | |
6 | 3 5 | syl6 | |
7 | 6 | a1i | |
8 | 7 | 3imp | |
9 | eqcom | |
|
10 | 1 | iota2 | |
11 | 10 | biimprd | |
12 | 9 11 | biimtrid | |
13 | 12 | impancom | |
14 | 13 | 3adant2 | |
15 | 8 14 | mpd | |