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

Proof

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