This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2rexreu

Description: Double restricted existential uniqueness implies double restricted unique existential quantification, analogous to 2exeu . (Contributed by Alexander van der Vekens, 25-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		reurmo	⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 )
2		reurex	⊢ ( ∃! 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑦 ∈ 𝐵 𝜑 )
3	2	rmoimi	⊢ ( ∃* 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 )
4	1 3	syl	⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 )
5		2reurex	⊢ ( ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 )
6	4 5	anim12ci	⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) → ( ∃ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ) )
7		reu5	⊢ ( ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 ) )
8	6 7	sylibr	⊢ ( ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) → ∃! 𝑥 ∈ 𝐴 ∃! 𝑦 ∈ 𝐵 𝜑 )