Description: Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvrex2v . (Contributed by Alexander van der Vekens, 2-Jul-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbvral2.1 | |
|
cbvral2.2 | |
||
cbvral2.3 | |
||
cbvral2.4 | |
||
cbvral2.5 | |
||
cbvral2.6 | |
||
Assertion | cbvrex2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvral2.1 | |
|
2 | cbvral2.2 | |
|
3 | cbvral2.3 | |
|
4 | cbvral2.4 | |
|
5 | cbvral2.5 | |
|
6 | cbvral2.6 | |
|
7 | nfcv | |
|
8 | 7 1 | nfrex | |
9 | nfcv | |
|
10 | 9 2 | nfrex | |
11 | 5 | rexbidv | |
12 | 8 10 11 | cbvrexw | |
13 | 3 4 6 | cbvrexw | |
14 | 13 | rexbii | |
15 | 12 14 | bitri | |