Theorem rmoeqd

Description: Equality deduction for restricted at-most-one quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017)

	Ref	Expression
Hypothesis	raleqd.1	$$⊢A=B\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	rmoeqd	$$⊢A=B\to \left({\exists }^{*}x\in A\phi \leftrightarrow {\exists }^{*}x\in B\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		raleqd.1	$$⊢A=B\to \left(\phi \leftrightarrow \psi \right)$$
2		rmoeq1	$$⊢A=B\to \left({\exists }^{*}x\in A\phi \leftrightarrow {\exists }^{*}x\in B\phi \right)$$
3	1	rmobidv	$$⊢A=B\to \left({\exists }^{*}x\in B\phi \leftrightarrow {\exists }^{*}x\in B\psi \right)$$
4	2 3	bitrd	$$⊢A=B\to \left({\exists }^{*}x\in A\phi \leftrightarrow {\exists }^{*}x\in B\psi \right)$$