Theorem rabeqiOLD

Description: Obsolete version of rabeqi as of 3-Jun-2024. (Contributed by Glauco Siliprandi, 26-Jun-2021) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 20-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	rabeqi.1	|- A = B
Assertion	rabeqiOLD	|- { x e. A | ph } = { x e. B | ph }

Proof

Step	Hyp	Ref	Expression
1		rabeqi.1	|- A = B
2	1	nfth	|- F/ x A = B
3		eleq2	|- ( A = B -> ( x e. A <-> x e. B ) )
4	3	anbi1d	|- ( A = B -> ( ( x e. A /\ ph ) <-> ( x e. B /\ ph ) ) )
5	2 4	abbid	|- ( A = B -> { x | ( x e. A /\ ph ) } = { x | ( x e. B /\ ph ) } )
6		df-rab	|- { x e. A | ph } = { x | ( x e. A /\ ph ) }
7		df-rab	|- { x e. B | ph } = { x | ( x e. B /\ ph ) }
8	5 6 7	3eqtr4g	|- ( A = B -> { x e. A | ph } = { x e. B | ph } )
9	1 8	ax-mp	|- { x e. A | ph } = { x e. B | ph }