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	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		n0i	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → ¬ ( 𝐵 ↑m 𝐶 ) = ∅ )
2		fnmap	⊢ ↑m Fn ( V × V )
3	2	fndmi	⊢ dom ↑m = ( V × V )
4	3	ndmov	⊢ ( ¬ ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐵 ↑m 𝐶 ) = ∅ )
5	1 4	nsyl2	⊢ ( 𝐴 ∈ ( 𝐵 ↑m 𝐶 ) → ( 𝐵 ∈ V ∧ 𝐶 ∈ V ) )