Description: Membership in a range. (Contributed by Mario Carneiro, 5-Nov-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | relelrnb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrng | |
|
2 | 1 | ibi | |
3 | relelrn | |
|
4 | 3 | ex | |
5 | 4 | exlimdv | |
6 | 2 5 | impbid2 | |