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 
|- 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 dfssf 
 |-  ( 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 ) )