Theorem rmoeqbii

Description: Equality inference for restricted at-most-one quantifier. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	rmoeqbii.1	$$⊢A=B$$
	rmoeqbii.2	$$⊢\psi \leftrightarrow \chi$$
Assertion	rmoeqbii	$$⊢{\exists }^{*}x\in A\psi \leftrightarrow {\exists }^{*}x\in B\chi$$

Proof

Step	Hyp	Ref	Expression
1		rmoeqbii.1	$$⊢A=B$$
2		rmoeqbii.2	$$⊢\psi \leftrightarrow \chi$$
3	1	eleq2i	$$⊢x\in A\leftrightarrow x\in B$$
4	3 2	anbi12i	$$⊢\left(x\in A\wedge \psi \right)\leftrightarrow \left(x\in B\wedge \chi \right)$$
5	4	mobii	$$⊢{\exists }^{*}x\left(x\in A\wedge \psi \right)\leftrightarrow {\exists }^{*}x\left(x\in B\wedge \chi \right)$$
6		df-rmo	$$⊢{\exists }^{*}x\in A\psi \leftrightarrow {\exists }^{*}x\left(x\in A\wedge \psi \right)$$
7		df-rmo	$$⊢{\exists }^{*}x\in B\chi \leftrightarrow {\exists }^{*}x\left(x\in B\wedge \chi \right)$$
8	5 6 7	3bitr4i	$$⊢{\exists }^{*}x\in A\psi \leftrightarrow {\exists }^{*}x\in B\chi$$