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\in \left(B^C\right)\to \left(B\in \mathrm{V}\wedge C\in \mathrm{V}\right)$$

Proof

Step	Hyp	Ref	Expression
1		n0i	$$⊢A\in \left(B^C\right)\to \neg B^C=\varnothing$$
2		fnmap	$$⊢{\uparrow }_{𝑚}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$
3	2	fndmi	$$⊢\mathrm{dom}{\uparrow }_{𝑚}=\mathrm{V}\times \mathrm{V}$$
4	3	ndmov	$$⊢\neg \left(B\in \mathrm{V}\wedge C\in \mathrm{V}\right)\to B^C=\varnothing$$
5	1 4	nsyl2	$$⊢A\in \left(B^C\right)\to \left(B\in \mathrm{V}\wedge C\in \mathrm{V}\right)$$