Theorem rabrabiOLD

Description: Obsolete version of rabrabi as of 12-Oct-2024. (Contributed by AV, 2-Aug-2022) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 20-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	rabrabiOLD.1	|- ( x = y -> ( ch <-> ph ) )
Assertion	rabrabiOLD	|- { x e. { y e. A | ph } | ps } = { x e. A | ( ch /\ ps ) }

Proof

Step	Hyp	Ref	Expression
1		rabrabiOLD.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 ) }