Theorem riotaeqbii

Description: Equivalent wff's and equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	riotaeqbii.1	$$⊢A=B$$
	riotaeqbii.2	$$⊢\phi \leftrightarrow \psi$$
Assertion	riotaeqbii	$$⊢\left(\iota x\in A|\phi \right)=\left(\iota x\in B|\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		riotaeqbii.1	$$⊢A=B$$
2		riotaeqbii.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	iotabii	$$⊢\left(\iota x|\left(x\in A\wedge \phi \right)\right)=\left(\iota x|\left(x\in B\wedge \psi \right)\right)$$
6		df-riota	$$⊢\left(\iota x\in A|\phi \right)=\left(\iota x|\left(x\in A\wedge \phi \right)\right)$$
7		df-riota	$$⊢\left(\iota x\in B|\psi \right)=\left(\iota x|\left(x\in B\wedge \psi \right)\right)$$
8	5 6 7	3eqtr4i	$$⊢\left(\iota x\in A|\phi \right)=\left(\iota x\in B|\psi \right)$$