Theorem 2rmorex

Description: Double restricted quantification with "at most one", analogous to 2moex . (Contributed by Alexander van der Vekens, 17-Jun-2017)

	Ref	Expression
Assertion	2rmorex	⊢ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		nfcv	⊢ Ⅎ 𝑦 𝐴
2		nfre1	⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝐵 𝜑
3	1 2	nfrmow	⊢ Ⅎ 𝑦 ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑
4		rmoim	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → ∃ 𝑦 ∈ 𝐵 𝜑 ) → ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜑 ) )
5		rspe	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ∃ 𝑦 ∈ 𝐵 𝜑 )
6	5	ex	⊢ ( 𝑦 ∈ 𝐵 → ( 𝜑 → ∃ 𝑦 ∈ 𝐵 𝜑 ) )
7	6	ralrimivw	⊢ ( 𝑦 ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 ( 𝜑 → ∃ 𝑦 ∈ 𝐵 𝜑 ) )
8	4 7	syl11	⊢ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ( 𝑦 ∈ 𝐵 → ∃* 𝑥 ∈ 𝐴 𝜑 ) )
9	3 8	ralrimi	⊢ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∀ 𝑦 ∈ 𝐵 ∃* 𝑥 ∈ 𝐴 𝜑 )