Description: Restricted specialization, with two quantifiers. (Contributed by NM, 11-Feb-1997)
Ref | Expression | ||
---|---|---|---|
Assertion | rsp2 | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rsp | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 → ( 𝑥 ∈ 𝐴 → ∀ 𝑦 ∈ 𝐵 𝜑 ) ) | |
2 | rsp | ⊢ ( ∀ 𝑦 ∈ 𝐵 𝜑 → ( 𝑦 ∈ 𝐵 → 𝜑 ) ) | |
3 | 1 2 | syl6 | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝑦 ∈ 𝐵 → 𝜑 ) ) ) |
4 | 3 | impd | ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝜑 ) ) |