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 | |- F/ x ph |
|
rexlim2d.y | |- F/ y ph |
||
rexlim2d.3 | |- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) ) |
||
Assertion | rexlim2d | |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlim2d.x | |- F/ x ph |
|
2 | rexlim2d.y | |- F/ y ph |
|
3 | rexlim2d.3 | |- ( ph -> ( ( x e. A /\ y e. B ) -> ( ps -> ch ) ) ) |
|
4 | nfv | |- F/ x ch |
|
5 | nfv | |- F/ y x e. A |
|
6 | 2 5 | nfan | |- F/ y ( ph /\ x e. A ) |
7 | nfv | |- F/ y ch |
|
8 | 3 | expdimp | |- ( ( ph /\ x e. A ) -> ( y e. B -> ( ps -> ch ) ) ) |
9 | 6 7 8 | rexlimd | |- ( ( ph /\ x e. A ) -> ( E. y e. B ps -> ch ) ) |
10 | 9 | ex | |- ( ph -> ( x e. A -> ( E. y e. B ps -> ch ) ) ) |
11 | 1 4 10 | rexlimd | |- ( ph -> ( E. x e. A E. y e. B ps -> ch ) ) |