Theorem rmoi

Description: Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012) (Revised by NM, 16-Jun-2017)

	Ref	Expression
Hypotheses	rmoi.b	$$⊢x=B\to \left(\phi \leftrightarrow \psi \right)$$
	rmoi.c	$$⊢x=C\to \left(\phi \leftrightarrow \chi \right)$$
Assertion	rmoi	$$⊢\left({\exists }^{*}x\in A\phi \wedge \left(B\in A\wedge \psi \right)\wedge \left(C\in A\wedge \chi \right)\right)\to B=C$$

Proof

Step	Hyp	Ref	Expression
1		rmoi.b	$$⊢x=B\to \left(\phi \leftrightarrow \psi \right)$$
2		rmoi.c	$$⊢x=C\to \left(\phi \leftrightarrow \chi \right)$$
3	1 2	rmob	$$⊢\left({\exists }^{*}x\in A\phi \wedge \left(B\in A\wedge \psi \right)\right)\to \left(B=C\leftrightarrow \left(C\in A\wedge \chi \right)\right)$$
4	3	biimp3ar	$$⊢\left({\exists }^{*}x\in A\phi \wedge \left(B\in A\wedge \psi \right)\wedge \left(C\in A\wedge \chi \right)\right)\to B=C$$