Theorem rmoi2

Description: Consequence of "restricted at most one". (Contributed by Thierry Arnoux, 9-Dec-2019)

	Ref	Expression
Hypotheses	rmoi2.1	$$⊢x=B\to \left(\psi \leftrightarrow \chi \right)$$
	rmoi2.2	$$⊢\phi \to B\in A$$
	rmoi2.3	$$⊢\phi \to {\exists }^{*}x\in A\psi$$
	rmoi2.4	$$⊢\phi \to x\in A$$
	rmoi2.5	$$⊢\phi \to \psi$$
	rmoi2.6	$$⊢\phi \to \chi$$
Assertion	rmoi2	$$⊢\phi \to x=B$$

Proof

Step	Hyp	Ref	Expression
1		rmoi2.1	$$⊢x=B\to \left(\psi \leftrightarrow \chi \right)$$
2		rmoi2.2	$$⊢\phi \to B\in A$$
3		rmoi2.3	$$⊢\phi \to {\exists }^{*}x\in A\psi$$
4		rmoi2.4	$$⊢\phi \to x\in A$$
5		rmoi2.5	$$⊢\phi \to \psi$$
6		rmoi2.6	$$⊢\phi \to \chi$$
7	1 2 3 4 5	rmob2	$$⊢\phi \to \left(x=B\leftrightarrow \chi \right)$$
8	6 7	mpbird	$$⊢\phi \to x=B$$