Definition df-2reu

Description: Define the double restricted existential uniqueness quantifier. (Contributed by Thierry Arnoux, 4-Jul-2023)

	Ref	Expression
Assertion	df-2reu	⊢ ( ∃! 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 𝜑 ↔ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		cA	⊢ 𝐴
2		vy	⊢ 𝑦
3		cB	⊢ 𝐵
4		wph	⊢ 𝜑
5	4 0 2 1 3	w2reu	⊢ ∃! 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 𝜑
6	4 2 3	wrex	⊢ ∃ 𝑦 ∈ 𝐵 𝜑
7	6 0 1	wreu	⊢ ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑
8	4 0 1	wrex	⊢ ∃ 𝑥 ∈ 𝐴 𝜑
9	8 2 3	wreu	⊢ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑
10	7 9	wa	⊢ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 )
11	5 10	wb	⊢ ( ∃! 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 𝜑 ↔ ( ∃! 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ∧ ∃! 𝑦 ∈ 𝐵 ∃ 𝑥 ∈ 𝐴 𝜑 ) )