Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Cf. reuxfr1ds . (Contributed by Thierry Arnoux, 7-Apr-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | reuxfr1d.1 | |
|
reuxfr1d.2 | |
||
reuxfr1d.3 | |
||
Assertion | reuxfr1d | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reuxfr1d.1 | |
|
2 | reuxfr1d.2 | |
|
3 | reuxfr1d.3 | |
|
4 | reurex | |
|
5 | 2 4 | syl | |
6 | 5 | biantrurd | |
7 | r19.41v | |
|
8 | 3 | pm5.32da | |
9 | 8 | rexbidv | |
10 | 7 9 | bitr3id | |
11 | 10 | adantr | |
12 | 6 11 | bitrd | |
13 | 12 | reubidva | |
14 | reurmo | |
|
15 | 2 14 | syl | |
16 | 1 15 | reuxfrd | |
17 | 13 16 | bitrd | |