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 | |
|
Assertion | iota2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iota2.1 | |
|
2 | elex | |
|
3 | simpl | |
|
4 | simpr | |
|
5 | 1 | adantl | |
6 | nfv | |
|
7 | nfeu1 | |
|
8 | 6 7 | nfan | |
9 | nfvd | |
|
10 | nfcvd | |
|
11 | 3 4 5 8 9 10 | iota2df | |
12 | 2 11 | sylan | |