Theorem 2reu2

Description: Double restricted existential uniqueness, analogous to 2eu2 . (Contributed by Alexander van der Vekens, 29-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		reurmo	⊢ ( ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 → ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 )
2		2rmorex	⊢ ( ∃* 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 → ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 )
3		2reu1	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) ) )
4		simpl	⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) → ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 )
5	3 4	syl6bi	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃* 𝑦 ∈ 𝐵 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 → ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) )
6	1 2 5	3syl	⊢ ( ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 → ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) )
7		2rexreu	⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) → ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 )
8	7	expcom	⊢ ( ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ) )
9	6 8	impbid	⊢ ( ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 → ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ) )