ssrmof

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

	Ref	Expression
Hypotheses	ssrexf.1	$⊢ \underline{Ⅎ} x A$
	ssrexf.2	$⊢ \underline{Ⅎ} x B$
Assertion	ssrmof	$⊢ A \subseteq B \to (\exists^{} x \in B φ \to \exists^{} x \in A φ)$

Step	Hyp	Ref	Expression
1		ssrexf.1	$⊢ \underline{Ⅎ} x A$
2		ssrexf.2	$⊢ \underline{Ⅎ} x B$
3	1 2	dfssf	$⊢ A \subseteq B \leftrightarrow \forall x (x \in A \to x \in B)$
4	3	biimpi	$⊢ A \subseteq B \to \forall x (x \in A \to x \in B)$
5		pm3.45	$⊢ (x \in A \to x \in B) \to ((x \in A \land φ) \to (x \in B \land φ))$
6	5	alimi	$⊢ \forall x (x \in A \to x \in B) \to \forall x ((x \in A \land φ) \to (x \in B \land φ))$
7		moim	$⊢ \forall x ((x \in A \land φ) \to (x \in B \land φ)) \to (\exists^{} x (x \in B \land φ) \to \exists^{} x (x \in A \land φ))$
8	4 6 7	3syl	$⊢ A \subseteq B \to (\exists^{} x (x \in B \land φ) \to \exists^{} x (x \in A \land φ))$
9		df-rmo	$⊢ \exists^{} x \in B φ \leftrightarrow \exists^{} x (x \in B \land φ)$
10		df-rmo	$⊢ \exists^{} x \in A φ \leftrightarrow \exists^{} x (x \in A \land φ)$
11	8 9 10	3imtr4g	$⊢ A \subseteq B \to (\exists^{} x \in B φ \to \exists^{} x \in A φ)$

Metamath Proof Explorer