Definition df-2reu 30238

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 30237	. 2 wff ∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑
7	1, 3, 5	wrex 3138	. . . 4 wff ∃𝑦 ∈ 𝐵 𝜑
8	7, 2, 4	wreu 3139	. . 3 wff ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑
9	1, 2, 4	wrex 3138	. . . 4 wff ∃𝑥 ∈ 𝐴 𝜑
10	9, 3, 5	wreu 3139	. . 3 wff ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑
11	8, 10	wa 398	. 2 wff (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑)
12	6, 11	wb 208	1 wff (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))

This definition is referenced by:  2reucom  30239  2reu2rex1  30240  2reureurex  30241  2reu2reu2  30242  opreu2reu1  30243  sq2reunnltb  30244  addsqnot2reu  30245