Metamath Proof Explorer

Theorem elpmi2

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

Ref Expression
Assertion elpmi2 F A 𝑝𝑚 B dom F B


Step Hyp Ref Expression
1 elpmi F A 𝑝𝑚 B F : dom F A dom F B
2 1 simprd F A 𝑝𝑚 B dom F B