Theorem rabrabi

Description: Abstract builder restricted to another restricted abstract builder with implicit substitution. (Contributed by AV, 2-Aug-2022) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 20-Aug-2023)

	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	1	cbvrabv	|- { x e. A | ch } = { y e. A | ph }
3	2	rabeqi	|- { x e. { x e. A | ch } | ps } = { x e. { y e. A | ph } | ps }
4		rabrab	|- { x e. { x e. A | ch } | ps } = { x e. A | ( ch /\ ps ) }
5	3 4	eqtr3i	|- { x e. { y e. A | ph } | ps } = { x e. A | ( ch /\ ps ) }