Definition df-2reu 30827

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

This definition is referenced by:  2reucom  30828  2reu2rex1  30829  2reureurex  30830  2reu2reu2  30831  opreu2reu1  30832  sq2reunnltb  30833  addsqnot2reu  30834