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