Definition df-2reu 30728

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 30727	. 2 wff ∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑
7	1, 3, 5	wrex 3064	. . . 4 wff ∃𝑦 ∈ 𝐵 𝜑
8	7, 2, 4	wreu 3065	. . 3 wff ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑
9	1, 2, 4	wrex 3064	. . . 4 wff ∃𝑥 ∈ 𝐴 𝜑
10	9, 3, 5	wreu 3065	. . 3 wff ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑
11	8, 10	wa 395	. 2 wff (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
12	6, 11	wb 205	1 wff (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))

This definition is referenced by:  2reucom  30729  2reu2rex1  30730  2reureurex  30731  2reu2reu2  30732  opreu2reu1  30733  sq2reunnltb  30734  addsqnot2reu  30735