This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ∃! 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜓 } 𝜒 ↔ ∃! 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜒 ) )