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 | ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜓 → 𝜒 ) ) |