Description: Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 15-Oct-2016) (Revised by Gino Giotto, 10-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cbvreuw.1 | |
|
cbvreuw.2 | |
||
cbvreuw.3 | |
||
Assertion | cbvreuw | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvreuw.1 | |
|
2 | cbvreuw.2 | |
|
3 | cbvreuw.3 | |
|
4 | nfv | |
|
5 | 4 | sb8euv | |
6 | sban | |
|
7 | 6 | eubii | |
8 | clelsb1 | |
|
9 | 8 | anbi1i | |
10 | 9 | eubii | |
11 | nfv | |
|
12 | 1 | nfsbv | |
13 | 11 12 | nfan | |
14 | nfv | |
|
15 | eleq1w | |
|
16 | sbequ | |
|
17 | 2 3 | sbiev | |
18 | 16 17 | bitrdi | |
19 | 15 18 | anbi12d | |
20 | 13 14 19 | cbveuw | |
21 | 10 20 | bitri | |
22 | 5 7 21 | 3bitri | |
23 | df-reu | |
|
24 | df-reu | |
|
25 | 22 23 24 | 3bitr4i | |