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 e. ( B ^m C ) -> ( B e. _V /\ C e. _V ) )

Proof

Step	Hyp	Ref	Expression
1		n0i	|- ( A e. ( B ^m C ) -> -. ( B ^m C ) = (/) )
2		fnmap	|- ^m Fn ( _V X. _V )
3	2	fndmi	|- dom ^m = ( _V X. _V )
4	3	ndmov	|- ( -. ( B e. _V /\ C e. _V ) -> ( B ^m C ) = (/) )
5	1 4	nsyl2	|- ( A e. ( B ^m C ) -> ( B e. _V /\ C e. _V ) )