Description: Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch to see if this will shorten proofs. (Contributed by NM, 24-May-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | lspexchn2.v | |
|
lspexchn2.n | |
||
lspexchn2.w | |
||
lspexchn2.x | |
||
lspexchn2.y | |
||
lspexchn2.z | |
||
lspexchn2.q | |
||
lspexchn2.e | |
||
Assertion | lspexchn2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lspexchn2.v | |
|
2 | lspexchn2.n | |
|
3 | lspexchn2.w | |
|
4 | lspexchn2.x | |
|
5 | lspexchn2.y | |
|
6 | lspexchn2.z | |
|
7 | lspexchn2.q | |
|
8 | lspexchn2.e | |
|
9 | prcom | |
|
10 | 9 | fveq2i | |
11 | 10 | eleq2i | |
12 | 8 11 | sylnib | |
13 | 1 2 3 4 5 6 7 12 | lspexchn1 | |
14 | prcom | |
|
15 | 14 | fveq2i | |
16 | 15 | eleq2i | |
17 | 13 16 | sylnib | |