Description: Rule used to change the bound variable in a restricted existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017) Avoid ax-9 , ax-ext . (Revised by Wolf Lammen, 9-Mar-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | cbvraldva.1 | ||
Assertion | cbvrexdva |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbvraldva.1 | ||
2 | 1 | notbid | |
3 | 2 | cbvraldva | |
4 | ralnex | ||
5 | ralnex | ||
6 | 3 4 5 | 3bitr3g | |
7 | 6 | con4bid |