Theorem rabeqbii

Description: Equality theorem for restricted class abstractions. Inference version. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	rabeqbii.1	$$⊢A=B$$
	rabeqbii.2	$$⊢\phi \leftrightarrow \psi$$
Assertion	rabeqbii	$$⊢\left\{x\in A|\phi \right\}=\left\{x\in B|\psi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		rabeqbii.1	$$⊢A=B$$
2		rabeqbii.2	$$⊢\phi \leftrightarrow \psi$$
3	1	eleq2i	$$⊢x\in A\leftrightarrow x\in B$$
4	3 2	anbi12i	$$⊢\left(x\in A\wedge \phi \right)\leftrightarrow \left(x\in B\wedge \psi \right)$$
5	4	abbii	$$⊢\left\{x|\left(x\in A\wedge \phi \right)\right\}=\left\{x|\left(x\in B\wedge \psi \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|\psi \right\}=\left\{x|\left(x\in B\wedge \psi \right)\right\}$$
8	5 6 7	3eqtr4i	$$⊢\left\{x\in A|\phi \right\}=\left\{x\in B|\psi \right\}$$