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

Metamath Proof Explorer

Theorem riotarab

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

Ref Expression
Hypothesis riotarab.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion riotarab ( ℩ 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜓 } 𝜒 ) = ( ℩ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜒 ) )

Proof

Step Hyp Ref Expression
1 riotarab.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2 1 bicomd ⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜑 ) )
3 2 equcoms ⊢ ( 𝑦 = 𝑥 → ( 𝜓 ↔ 𝜑 ) )
4 3 elrab ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜓 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
5 4 anbi1i ⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜓 } ∧ 𝜒 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ 𝜒 ) )
6 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∧ 𝜒 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝜒 ) ) )
7 5 6 bitri ⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜓 } ∧ 𝜒 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝜒 ) ) )
8 7 iotabii ⊢ ( ℩ 𝑥 ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜓 } ∧ 𝜒 ) ) = ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝜒 ) ) )
9 df-riota ⊢ ( ℩ 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜓 } 𝜒 ) = ( ℩ 𝑥 ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜓 } ∧ 𝜒 ) )
10 df-riota ⊢ ( ℩ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜒 ) ) = ( ℩ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∧ 𝜒 ) ) )
11 8 9 10 3eqtr4i ⊢ ( ℩ 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜓 } 𝜒 ) = ( ℩ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜒 ) )