Description: Transfer universal quantification from a variable x to another variable y contained in expression A . (Contributed by NM, 15-Aug-2014) (Proof shortened by Mario Carneiro, 19-Nov-2016) (Proof shortened by JJ, 7-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ralxfrd.1 | |
|
ralxfrd.2 | |
||
ralxfrd.3 | |
||
Assertion | ralxfrd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralxfrd.1 | |
|
2 | ralxfrd.2 | |
|
3 | ralxfrd.3 | |
|
4 | 3 | adantlr | |
5 | 1 4 | rspcdv | |
6 | 5 | ralrimdva | |
7 | r19.29 | |
|
8 | 3 | exbiri | |
9 | 8 | impcomd | |
10 | 9 | rexlimdvw | |
11 | 7 10 | syl5 | |
12 | 11 | adantr | |
13 | 2 12 | mpan2d | |
14 | 13 | ralrimdva | |
15 | 6 14 | impbid | |