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	rabeqiOLD.1	$$⊢A=B$$
Assertion	rabeqiOLD	$$⊢\left\{x\in A|\phi \right\}=\left\{x\in B|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		rabeqiOLD.1	$$⊢A=B$$
2	1	nfth	$$⊢ℲxA=B$$
3		eleq2	$$⊢A=B\to \left(x\in A\leftrightarrow x\in B\right)$$
4	3	anbi1d	$$⊢A=B\to \left(\left(x\in A\wedge \phi \right)\leftrightarrow \left(x\in B\wedge \phi \right)\right)$$
5	2 4	abbid	$$⊢A=B\to \left\{x|\left(x\in A\wedge \phi \right)\right\}=\left\{x|\left(x\in B\wedge \phi \right)\right\}$$
6		df-rab	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\left(x\in A\wedge \phi \right)\right\}$$
7		df-rab	$$⊢\left\{x\in B|\phi \right\}=\left\{x|\left(x\in B\wedge \phi \right)\right\}$$
8	5 6 7	3eqtr4g	$$⊢A=B\to \left\{x\in A|\phi \right\}=\left\{x\in B|\phi \right\}$$
9	1 8	ax-mp	$$⊢\left\{x\in A|\phi \right\}=\left\{x\in B|\phi \right\}$$