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 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
Assertion reurab ( ∃! 𝑥 ∈ { 𝑦𝐴𝜓 } 𝜒 ↔ ∃! 𝑥𝐴 ( 𝜑𝜒 ) )

Proof

Step Hyp Ref Expression
1 reurab.1 ( 𝑥 = 𝑦 → ( 𝜑𝜓 ) )
2 1 bicomd ( 𝑥 = 𝑦 → ( 𝜓𝜑 ) )
3 2 equcoms ( 𝑦 = 𝑥 → ( 𝜓𝜑 ) )
4 3 elrab ( 𝑥 ∈ { 𝑦𝐴𝜓 } ↔ ( 𝑥𝐴𝜑 ) )
5 4 anbi1i ( ( 𝑥 ∈ { 𝑦𝐴𝜓 } ∧ 𝜒 ) ↔ ( ( 𝑥𝐴𝜑 ) ∧ 𝜒 ) )
6 anass ( ( ( 𝑥𝐴𝜑 ) ∧ 𝜒 ) ↔ ( 𝑥𝐴 ∧ ( 𝜑𝜒 ) ) )
7 5 6 bitri ( ( 𝑥 ∈ { 𝑦𝐴𝜓 } ∧ 𝜒 ) ↔ ( 𝑥𝐴 ∧ ( 𝜑𝜒 ) ) )
8 7 eubii ( ∃! 𝑥 ( 𝑥 ∈ { 𝑦𝐴𝜓 } ∧ 𝜒 ) ↔ ∃! 𝑥 ( 𝑥𝐴 ∧ ( 𝜑𝜒 ) ) )
9 df-reu ( ∃! 𝑥 ∈ { 𝑦𝐴𝜓 } 𝜒 ↔ ∃! 𝑥 ( 𝑥 ∈ { 𝑦𝐴𝜓 } ∧ 𝜒 ) )
10 df-reu ( ∃! 𝑥𝐴 ( 𝜑𝜒 ) ↔ ∃! 𝑥 ( 𝑥𝐴 ∧ ( 𝜑𝜒 ) ) )
11 8 9 10 3bitr4i ( ∃! 𝑥 ∈ { 𝑦𝐴𝜓 } 𝜒 ↔ ∃! 𝑥𝐴 ( 𝜑𝜒 ) )