Theorem 2reurmo

Description: Double restricted quantification with restricted existential uniqueness and restricted "at most one", analogous to 2eumo . (Contributed by Alexander van der Vekens, 24-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		reuimrmo	⊢ ( ∀ 𝑥 ∈ 𝐴 ( ∃! 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑦 ∈ 𝐵 𝜑 ) → ( ∃! 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ) )
2		reurmo	⊢ ( ∃! 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑦 ∈ 𝐵 𝜑 )
3	2	a1i	⊢ ( 𝑥 ∈ 𝐴 → ( ∃! 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑦 ∈ 𝐵 𝜑 ) )
4	1 3	mprg	⊢ ( ∃! 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 )