ustimasn

		Ref	Expression
	Assertion	ustimasn	$⊢ (U \in UnifOn (X) \land V \in U \land P \in X) \to V [\{P\}] \subseteq X$

Step	Hyp	Ref	Expression
1		imassrn	$⊢ V [\{P\}] \subseteq ran V$
2		ustssxp	$⊢ (U \in UnifOn (X) \land V \in U) \to V \subseteq X \times X$
3	2	3adant3	$⊢ (U \in UnifOn (X) \land V \in U \land P \in X) \to V \subseteq X \times X$
4		rnss	$⊢ V \subseteq X \times X \to ran V \subseteq ran (X \times X)$
5		rnxpid	$⊢ ran (X \times X) = X$
6	4 5	sseqtrdi	$⊢ V \subseteq X \times X \to ran V \subseteq X$
7	3 6	syl	$⊢ (U \in UnifOn (X) \land V \in U \land P \in X) \to ran V \subseteq X$
8	1 7	sstrid	$⊢ (U \in UnifOn (X) \land V \in U \land P \in X) \to V [\{P\}] \subseteq X$

Metamath Proof Explorer