Metamath Proof Explorer

Theorem funpr

Description: A function with a domain of two elements. (Contributed by Jeff Madsen, 20-Jun-2010)

Ref Expression
Hypotheses funpr.1 A V
funpr.2 B V
funpr.3 C V
funpr.4 D V
Assertion funpr A B Fun A C B D


Step Hyp Ref Expression
1 funpr.1 A V
2 funpr.2 B V
3 funpr.3 C V
4 funpr.4 D V
5 1 2 pm3.2i A V B V
6 3 4 pm3.2i C V D V
7 funprg A V B V C V D V A B Fun A C B D
8 5 6 7 mp3an12 A B Fun A C B D