Theorem ssrmof

Description: "At most one" existential quantification restricted to a subclass. (Contributed by Thierry Arnoux, 8-Oct-2017)

	Ref	Expression
Hypotheses	ssrexf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	ssrexf.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	ssrmof	$$⊢A\subseteq B\to \left({\exists }^{*}x\in B\phi \to {\exists }^{*}x\in A\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ssrexf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		ssrexf.2	$$⊢\underset{\_}{Ⅎ}xB$$
3	1 2	dfss2f	$$⊢A\subseteq B\leftrightarrow \forall x\left(x\in A\to x\in B\right)$$
4	3	biimpi	$$⊢A\subseteq B\to \forall x\left(x\in A\to x\in B\right)$$
5		pm3.45	$$⊢\left(x\in A\to x\in B\right)\to \left(\left(x\in A\wedge \phi \right)\to \left(x\in B\wedge \phi \right)\right)$$
6	5	alimi	$$⊢\forall x\left(x\in A\to x\in B\right)\to \forall x\left(\left(x\in A\wedge \phi \right)\to \left(x\in B\wedge \phi \right)\right)$$
7		moim	$$⊢\forall x\left(\left(x\in A\wedge \phi \right)\to \left(x\in B\wedge \phi \right)\right)\to \left({\exists }^{*}x\left(x\in B\wedge \phi \right)\to {\exists }^{*}x\left(x\in A\wedge \phi \right)\right)$$
8	4 6 7	3syl	$$⊢A\subseteq B\to \left({\exists }^{*}x\left(x\in B\wedge \phi \right)\to {\exists }^{*}x\left(x\in A\wedge \phi \right)\right)$$
9		df-rmo	$$⊢{\exists }^{*}x\in B\phi \leftrightarrow {\exists }^{*}x\left(x\in B\wedge \phi \right)$$
10		df-rmo	$$⊢{\exists }^{*}x\in A\phi \leftrightarrow {\exists }^{*}x\left(x\in A\wedge \phi \right)$$
11	8 9 10	3imtr4g	$$⊢A\subseteq B\to \left({\exists }^{*}x\in B\phi \to {\exists }^{*}x\in A\phi \right)$$