Description: Existence version of disjen . (Contributed by Mario Carneiro, 7-Feb-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | disjenex | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | |
|
2 | snex | |
|
3 | xpexg | |
|
4 | 1 2 3 | sylancl | |
5 | disjen | |
|
6 | ineq2 | |
|
7 | 6 | eqeq1d | |
8 | breq1 | |
|
9 | 7 8 | anbi12d | |
10 | 4 5 9 | spcedv | |