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	|- ( x = y -> ( ch <-> ph ) )
Assertion	rabrabi	|- { x e. { y e. A | ph } | ps } = { x e. A | ( ch /\ ps ) }

Proof

Step	Hyp	Ref	Expression
1		rabrabi.1	|- ( x = y -> ( ch <-> ph ) )
2		df-rab	|- { y e. A | ph } = { y | ( y e. A /\ ph ) }
3	2	eleq2i	|- ( x e. { y e. A | ph } <-> x e. { y | ( y e. A /\ ph ) } )
4		df-clab	|- ( x e. { y | ( y e. A /\ ph ) } <-> [ x / y ] ( y e. A /\ ph ) )
5		eleq1w	|- ( y = x -> ( y e. A <-> x e. A ) )
6	1	bicomd	|- ( x = y -> ( ph <-> ch ) )
7	6	equcoms	|- ( y = x -> ( ph <-> ch ) )
8	5 7	anbi12d	|- ( y = x -> ( ( y e. A /\ ph ) <-> ( x e. A /\ ch ) ) )
9	8	sbievw	|- ( [ x / y ] ( y e. A /\ ph ) <-> ( x e. A /\ ch ) )
10	4 9	bitri	|- ( x e. { y | ( y e. A /\ ph ) } <-> ( x e. A /\ ch ) )
11	3 10	bitri	|- ( x e. { y e. A | ph } <-> ( x e. A /\ ch ) )
12	11	anbi1i	|- ( ( x e. { y e. A | ph } /\ ps ) <-> ( ( x e. A /\ ch ) /\ ps ) )
13		anass	|- ( ( ( x e. A /\ ch ) /\ ps ) <-> ( x e. A /\ ( ch /\ ps ) ) )
14	12 13	bitri	|- ( ( x e. { y e. A | ph } /\ ps ) <-> ( x e. A /\ ( ch /\ ps ) ) )
15	14	rabbia2	|- { x e. { y e. A | ph } | ps } = { x e. A | ( ch /\ ps ) }