Definition df-2reu 33075

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

Assertion

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

Detailed syntax breakdown of Definition df-2reu

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cA	. . 3 class 𝐴
5		cB	. . 3 class 𝐵
6	1, 2, 3, 4, 5	w2reu 33074	. 2 wff ∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑
7	1, 3, 5	wrex 3086	. . . 4 wff ∃𝑦 ∈ 𝐵 𝜑
8	7, 2, 4	wreu 3363	. . 3 wff ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑
9	1, 2, 4	wrex 3086	. . . 4 wff ∃𝑥 ∈ 𝐴 𝜑
10	9, 3, 5	wreu 3363	. . 3 wff ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑
11	8, 10	wa 401	. 2 wff (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
12	6, 11	wb 209	1 wff (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))

This definition is used by:  2reucom  33076  2reu2rex1  33077  2reureurex  33078  2reu2reu2  33079  opreu2reu1  33080  sq2reunnltb  33081  addsqnot2reu  33082