This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 dfssf ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
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 ⊢ ( 𝐴 ⊆ 𝐵 → ( ∃* 𝑥 ∈ 𝐵 𝜑 → ∃* 𝑥 ∈ 𝐴 𝜑 ) )