Description: Transfer "at most one" restricted quantification from a variable x to another variable y contained in expression A . (Contributed by Thierry Arnoux, 7-Apr-2017) (Revised by Thierry Arnoux, 8-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rmoxfrd.1 | |
|
rmoxfrd.2 | |
||
rmoxfrd.3 | |
||
Assertion | rmoxfrd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rmoxfrd.1 | |
|
2 | rmoxfrd.2 | |
|
3 | rmoxfrd.3 | |
|
4 | reurex | |
|
5 | 2 4 | syl | |
6 | 1 5 3 | rexxfrd | |
7 | df-rex | |
|
8 | df-rex | |
|
9 | 6 7 8 | 3bitr3g | |
10 | 1 2 3 | reuxfr1d | |
11 | df-reu | |
|
12 | df-reu | |
|
13 | 10 11 12 | 3bitr3g | |
14 | 9 13 | imbi12d | |
15 | moeu | |
|
16 | moeu | |
|
17 | 14 15 16 | 3bitr4g | |
18 | df-rmo | |
|
19 | df-rmo | |
|
20 | 17 18 19 | 3bitr4g | |