Theorem ssrmof

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

	Ref	Expression
Hypotheses	ssrexf.1	|- F/_ x A
	ssrexf.2	|- F/_ x B
Assertion	ssrmof	|- ( A C_ B -> ( E* x e. B ph -> E* x e. A ph ) )

Proof

Step	Hyp	Ref	Expression
1		ssrexf.1	|- F/_ x A
2		ssrexf.2	|- F/_ x B
3	1 2	dfss2f	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4	3	biimpi	|- ( A C_ B -> A. x ( x e. A -> x e. B ) )
5		pm3.45	|- ( ( x e. A -> x e. B ) -> ( ( x e. A /\ ph ) -> ( x e. B /\ ph ) ) )
6	5	alimi	|- ( A. x ( x e. A -> x e. B ) -> A. x ( ( x e. A /\ ph ) -> ( x e. B /\ ph ) ) )
7		moim	|- ( A. x ( ( x e. A /\ ph ) -> ( x e. B /\ ph ) ) -> ( E* x ( x e. B /\ ph ) -> E* x ( x e. A /\ ph ) ) )
8	4 6 7	3syl	|- ( A C_ B -> ( E* x ( x e. B /\ ph ) -> E* x ( x e. A /\ ph ) ) )
9		df-rmo	|- ( E* x e. B ph <-> E* x ( x e. B /\ ph ) )
10		df-rmo	|- ( E* x e. A ph <-> E* x ( x e. A /\ ph ) )
11	8 9 10	3imtr4g	|- ( A C_ B -> ( E* x e. B ph -> E* x e. A ph ) )