Metamath Proof Explorer


Theorem elpm2g

Description: The predicate "is a partial function." (Contributed by NM, 31-Dec-2013)

Ref Expression
Assertion elpm2g A V B W F A 𝑝𝑚 B F : dom F A dom F B

Proof

Step Hyp Ref Expression
1 elpmg A V B W F A 𝑝𝑚 B Fun F F B × A
2 funssxp Fun F F B × A F : dom F A dom F B
3 1 2 syl6bb A V B W F A 𝑝𝑚 B F : dom F A dom F B