Metamath Proof Explorer


Theorem 2reucom

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

Ref Expression
Assertion 2reucom Math input error

Proof

Step Hyp Ref Expression
1 ancom ∃!xAyBφ∃!yBxAφ∃!yBxAφ∃!xAyBφ
2 df-2reu Math input error
3 df-2reu Math input error
4 1 2 3 3bitr4i Math input error