Theorem riotaeqi

Description: Equal domains yield equal restricted iotas. Inference version. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypothesis	riotaeqi.1	$$⊢A=B$$
Assertion	riotaeqi	$$⊢\left(\iota x\in A|\phi \right)=\left(\iota x\in B|\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		riotaeqi.1	$$⊢A=B$$
2		biid	$$⊢\phi \leftrightarrow \phi$$
3	1 2	riotaeqbii	$$⊢\left(\iota x\in A|\phi \right)=\left(\iota x\in B|\phi \right)$$