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 ABCBVCV

Proof

Step Hyp Ref Expression
1 n0i ABC¬BC=
2 fnmap 𝑚FnV×V
3 2 fndmi dom𝑚=V×V
4 3 ndmov ¬BVCVBC=
5 1 4 nsyl2 ABCBVCV