Theorem 2reurex

Description: Double restricted quantification with existential uniqueness, analogous to 2euex . (Contributed by Alexander van der Vekens, 24-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		reu5	⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) )
2		rexcom	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 )
3		nfcv	⊢ Ⅎ 𝑦 𝐴
4		nfre1	⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝐵 𝜑
5	3 4	nfrmow	⊢ Ⅎ 𝑦 ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑
6		rspe	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ∃ 𝑦 ∈ 𝐵 𝜑 )
7	6	ex	⊢ ( 𝑦 ∈ 𝐵 → ( 𝜑 → ∃ 𝑦 ∈ 𝐵 𝜑 ) )
8	7	ralrimivw	⊢ ( 𝑦 ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 ( 𝜑 → ∃ 𝑦 ∈ 𝐵 𝜑 ) )
9		rmoim	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → ∃ 𝑦 ∈ 𝐵 𝜑 ) → ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜑 ) )
10	8 9	syl	⊢ ( 𝑦 ∈ 𝐵 → ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜑 ) )
11	10	impcom	⊢ ( ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ∃* 𝑥 ∈ 𝐴 𝜑 )
12		rmo5	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃! 𝑥 ∈ 𝐴 𝜑 ) )
13	11 12	sylib	⊢ ( ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃! 𝑥 ∈ 𝐴 𝜑 ) )
14	13	ex	⊢ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ( 𝑦 ∈ 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝜑 → ∃! 𝑥 ∈ 𝐴 𝜑 ) ) )
15	5 14	reximdai	⊢ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ( ∃ 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 ) )
16	2 15	syl5bi	⊢ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 ) )
17	16	impcom	⊢ ( ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) → ∃ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 )
18	1 17	sylbi	⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑦 ∈ 𝐵 ∃! 𝑥 ∈ 𝐴 𝜑 )