Metamath Proof Explorer


Theorem elmapex

Description: Eliminate antecedent for mapping theorems: domain can be taken to be a set. (Contributed by Stefan O'Rear, 8-Oct-2014)

Ref Expression
Assertion elmapex A B C B V C V

Proof

Step Hyp Ref Expression
1 n0i A B C ¬ B C =
2 fnmap 𝑚 Fn V × V
3 fndm 𝑚 Fn V × V dom 𝑚 = V × V
4 2 3 ax-mp dom 𝑚 = V × V
5 4 ndmov ¬ B V C V B C =
6 1 5 nsyl2 A B C B V C V