Metamath Proof Explorer


Theorem rsp2

Description: Restricted specialization, with two quantifiers. (Contributed by NM, 11-Feb-1997)

Ref Expression
Assertion rsp2 ( ∀ 𝑥𝐴𝑦𝐵 𝜑 → ( ( 𝑥𝐴𝑦𝐵 ) → 𝜑 ) )

Proof

Step Hyp Ref Expression
1 rsp ( ∀ 𝑥𝐴𝑦𝐵 𝜑 → ( 𝑥𝐴 → ∀ 𝑦𝐵 𝜑 ) )
2 rsp ( ∀ 𝑦𝐵 𝜑 → ( 𝑦𝐵𝜑 ) )
3 1 2 syl6 ( ∀ 𝑥𝐴𝑦𝐵 𝜑 → ( 𝑥𝐴 → ( 𝑦𝐵𝜑 ) ) )
4 3 impd ( ∀ 𝑥𝐴𝑦𝐵 𝜑 → ( ( 𝑥𝐴𝑦𝐵 ) → 𝜑 ) )