This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Step	Hyp	Ref	Expression
1		n0i	$⊢ A \in (B^{C}) \to \neg B^{C} = \emptyset$
2		fnmap	$⊢ ↑_{𝑚} Fn (V \times V)$
3	2	fndmi	$⊢ dom ↑_{𝑚} = V \times V$
4	3	ndmov	$⊢ \neg (B \in V \land C \in V) \to B^{C} = \emptyset$
5	1 4	nsyl2	$⊢ A \in (B^{C}) \to (B \in V \land C \in V)$