Theorem rsp2e

Description: Restricted specialization. (Contributed by FL, 4-Jun-2012) (Proof shortened by Wolf Lammen, 7-Jan-2020)

	Ref	Expression
Assertion	rsp2e	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		rspe	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ∃ 𝑦 ∈ 𝐵 𝜑 )
2		rspe	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 )
3	1 2	sylan2	⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 )
4	3	3impb	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 )