Theorem elpmi2

Description: The domain of a partial function. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Assertion	elpmi2	$$⊢F\in \left(A{\uparrow }_{𝑝𝑚}B\right)\to \mathrm{dom}F\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		elpmi	$$⊢F\in \left(A{\uparrow }_{𝑝𝑚}B\right)\to \left(F:\mathrm{dom}F⟶A\wedge \mathrm{dom}F\subseteq B\right)$$
2	1	simprd	$$⊢F\in \left(A{\uparrow }_{𝑝𝑚}B\right)\to \mathrm{dom}F\subseteq B$$