Definition df-2reu 32498

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

This definition is referenced by:  2reucom  32499  2reu2rex1  32500  2reureurex  32501  2reu2reu2  32502  opreu2reu1  32503  sq2reunnltb  32504  addsqnot2reu  32505