Description: Inference removing two restricted quantifiers. Same as rexlimdvv , but with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rexlim2d.x | ||
rexlim2d.y | |||
rexlim2d.3 | |||
Assertion | rexlim2d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlim2d.x | ||
2 | rexlim2d.y | ||
3 | rexlim2d.3 | ||
4 | nfv | ||
5 | nfv | ||
6 | 2 5 | nfan | |
7 | nfv | ||
8 | 3 | expdimp | |
9 | 6 7 8 | rexlimd | |
10 | 9 | ex | |
11 | 1 4 10 | rexlimd |