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 Gino Giotto, 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	4 9	bitri	⊢ ( 𝑥 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝜑 ) } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) )
11	3 10	bitri	⊢ ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) )
12	11	anbi1i	⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ∧ 𝜓 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ∧ 𝜓 ) )
13		anass	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝜒 ) ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝜒 ∧ 𝜓 ) ) )
14	12 13	bitri	⊢ ( ( 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝜒 ∧ 𝜓 ) ) )
15	14	rabbia2	⊢ { 𝑥 ∈ { 𝑦 ∈ 𝐴 ∣ 𝜑 } ∣ 𝜓 } = { 𝑥 ∈ 𝐴 ∣ ( 𝜒 ∧ 𝜓 ) }