Metamath Proof Explorer


Theorem 2reu2rex

Description: Double restricted existential uniqueness, analogous to 2eu2ex . (Contributed by Alexander van der Vekens, 25-Jun-2017)

Ref Expression
Assertion 2reu2rex ( ∃! 𝑥𝐴 ∃! 𝑦𝐵 𝜑 → ∃ 𝑥𝐴𝑦𝐵 𝜑 )

Proof

Step Hyp Ref Expression
1 reurex ( ∃! 𝑥𝐴 ∃! 𝑦𝐵 𝜑 → ∃ 𝑥𝐴 ∃! 𝑦𝐵 𝜑 )
2 reurex ( ∃! 𝑦𝐵 𝜑 → ∃ 𝑦𝐵 𝜑 )
3 2 reximi ( ∃ 𝑥𝐴 ∃! 𝑦𝐵 𝜑 → ∃ 𝑥𝐴𝑦𝐵 𝜑 )
4 1 3 syl ( ∃! 𝑥𝐴 ∃! 𝑦𝐵 𝜑 → ∃ 𝑥𝐴𝑦𝐵 𝜑 )