Description: Generalization rule for restricted quantification. Note that x and y needn't be distinct. (Contributed by Wolf Lammen, 10-Jun-2023)
Ref | Expression | ||
---|---|---|---|
Hypothesis | wl-rgenw.1 | ||
Assertion | wl-rgen2w |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wl-rgenw.1 | ||
2 | 1 | wl-rgenw | |
3 | 2 | wl-rgenw |