Theorem ssrmof

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

	Ref	Expression
Hypotheses	ssrexf.1	⊢ Ⅎ 𝑥 𝐴
	ssrexf.2	⊢ Ⅎ 𝑥 𝐵
Assertion	ssrmof	⊢ ( 𝐴 ⊆ 𝐵 → ( ∃* 𝑥 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		ssrexf.1	⊢ Ⅎ 𝑥 𝐴
2		ssrexf.2	⊢ Ⅎ 𝑥 𝐵
3	1 2	dfss2f	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
4	3	biimpi	⊢ ( 𝐴 ⊆ 𝐵 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
5		pm3.45	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
6	5	alimi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) → ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) )
7		moim	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) → ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) ) → ( ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
8	4 6 7	3syl	⊢ ( 𝐴 ⊆ 𝐵 → ( ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) → ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
9		df-rmo	⊢ ( ∃* 𝑥 ∈ 𝐵 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝜑 ) )
10		df-rmo	⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) )
11	8 9 10	3imtr4g	⊢ ( 𝐴 ⊆ 𝐵 → ( ∃* 𝑥 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜑 ) )