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