Metamath Proof Explorer


Theorem reurab

Description: Restricted existential uniqueness of a restricted abstraction. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Hypothesis reurab.1 x = y φ ψ
Assertion reurab ∃! x y A | ψ χ ∃! x A φ χ

Proof

Step Hyp Ref Expression
1 reurab.1 x = y φ ψ
2 1 bicomd x = y ψ φ
3 2 equcoms y = x ψ φ
4 3 elrab x y A | ψ x A φ
5 4 anbi1i x y A | ψ χ x A φ χ
6 anass x A φ χ x A φ χ
7 5 6 bitri x y A | ψ χ x A φ χ
8 7 eubii ∃! x x y A | ψ χ ∃! x x A φ χ
9 df-reu ∃! x y A | ψ χ ∃! x x y A | ψ χ
10 df-reu ∃! x A φ χ ∃! x x A φ χ
11 8 9 10 3bitr4i ∃! x y A | ψ χ ∃! x A φ χ