Theorem 2reucom 32488

Description: Double restricted existential uniqueness commutes. (Contributed by Thierry Arnoux, 4-Jul-2023.)

Assertion

Ref	Expression
2reucom	⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ ∃!𝑦 ∈ 𝐵 , 𝑥 ∈ 𝐴𝜑)

Proof of Theorem 2reucom

Step	Hyp	Ref	Expression
1		ancom 460	. 2 ⊢ ((∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑) ↔ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
2		df-2reu 32487	. 2 ⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ (∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑 ∧ ∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑))
3		df-2reu 32487	. 2 ⊢ (∃!𝑦 ∈ 𝐵 , 𝑥 ∈ 𝐴𝜑 ↔ (∃!𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝜑 ∧ ∃!𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜑))
4	1, 2, 3	3bitr4i 303	1 ⊢ (∃!𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵𝜑 ↔ ∃!𝑦 ∈ 𝐵 , 𝑥 ∈ 𝐴𝜑)

Syntax hints:   ↔ wb 206   ∧ wa 395  ∃wrex 3069  ∃!wreu 3377  ∃!w2reu 32486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-2reu 32487

This theorem is referenced by: (None)