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

Metamath Proof Explorer

Theorem rabrabi

Description: Abstract builder restricted to another restricted abstract builder with implicit substitution. (Contributed by AV, 2-Aug-2022) Avoid ax-10 , ax-11 and ax-12 . (Revised by GG, 12-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 rabrabi.1 ⊢ ( 𝑥 = 𝑦 → ( 𝜒 ↔ 𝜑 ) )
2 df-rab ⊢ { 𝑦 ∈ 𝐴 ∣ 𝜑 } = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) }
3 2 eleq2i ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ↔ 𝑥 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } )
4 df-clab ⊢ ( 𝑥 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } ↔ [ 𝑥 / 𝑦 ] ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) )
5 eleq1w ⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
6 1 bicomd ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
7 6 equcoms ⊢ ( 𝑦 = 𝑥 → ( 𝜑 ↔ 𝜒 ) )
8 5 7 anbi12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ) )
9 8 sbievw ⊢ ( [ 𝑥 / 𝑦 ] ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) )
10 3 4 9 3bitri ⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) )
11 10 anbi1i ⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ∧ 𝜓 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ∧ 𝜓 ) )
12 anass ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝜒 ∧ 𝜓 ) ) )
13 11 12 bitri ⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝜒 ∧ 𝜓 ) ) )
14 13 rabbia2 ⊢ { 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ∣ 𝜓 } = { 𝑥 ∈ 𝐴 ∣ ( 𝜒 ∧ 𝜓 ) }