Theorem rmob2

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$$
Assertion	rmob2	$$⊢\phi \to \left(x=B\leftrightarrow \chi \right)$$

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		df-rmo	$$⊢{\exists }^{*}x\in A\psi \leftrightarrow {\exists }^{*}x\left(x\in A\wedge \psi \right)$$
7	3 6	sylib	$$⊢\phi \to {\exists }^{*}x\left(x\in A\wedge \psi \right)$$
8		eleq1	$$⊢x=B\to \left(x\in A\leftrightarrow B\in A\right)$$
9	8 1	anbi12d	$$⊢x=B\to \left(\left(x\in A\wedge \psi \right)\leftrightarrow \left(B\in A\wedge \chi \right)\right)$$
10	9	mob2	$$⊢\left(B\in A\wedge {\exists }^{*}x\left(x\in A\wedge \psi \right)\wedge \left(x\in A\wedge \psi \right)\right)\to \left(x=B\leftrightarrow \left(B\in A\wedge \chi \right)\right)$$
11	2 7 4 5 10	syl112anc	$$⊢\phi \to \left(x=B\leftrightarrow \left(B\in A\wedge \chi \right)\right)$$
12	2 11	mpbirand	$$⊢\phi \to \left(x=B\leftrightarrow \chi \right)$$