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

Metamath Proof Explorer

Theorem moriotass

Description: Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006) (Revised by NM, 16-Jun-2017)

Ref Expression
Assertion moriotass 
|- ( ( A C_ B /\ E. x e. A ph /\ E* x e. B ph ) -> ( iota_ x e. A ph ) = ( iota_ x e. B ph ) )

Proof

Step Hyp Ref Expression
1 ssrexv 
 |-  ( A C_ B -> ( E. x e. A ph -> E. x e. B ph ) )
2 1 imp 
 |-  ( ( A C_ B /\ E. x e. A ph ) -> E. x e. B ph )
3 2 3adant3 
 |-  ( ( A C_ B /\ E. x e. A ph /\ E* x e. B ph ) -> E. x e. B ph )
4 simp3 
 |-  ( ( A C_ B /\ E. x e. A ph /\ E* x e. B ph ) -> E* x e. B ph )
5 reu5 
 |-  ( E! x e. B ph <-> ( E. x e. B ph /\ E* x e. B ph ) )
6 3 4 5 sylanbrc 
 |-  ( ( A C_ B /\ E. x e. A ph /\ E* x e. B ph ) -> E! x e. B ph )
7 riotass 
 |-  ( ( A C_ B /\ E. x e. A ph /\ E! x e. B ph ) -> ( iota_ x e. A ph ) = ( iota_ x e. B ph ) )
8 6 7 syld3an3 
 |-  ( ( A C_ B /\ E. x e. A ph /\ E* x e. B ph ) -> ( iota_ x e. A ph ) = ( iota_ x e. B ph ) )