Theorem elmapsnd

Description: Membership in a set exponentiated to a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	elmapsnd.1	|- ( ph -> F Fn { A } )
	elmapsnd.2	|- ( ph -> B e. V )
	elmapsnd.3	|- ( ph -> ( F ` A ) e. B )
Assertion	elmapsnd	|- ( ph -> F e. ( B ^m { A } ) )

Proof

Step	Hyp	Ref	Expression
1		elmapsnd.1	|- ( ph -> F Fn { A } )
2		elmapsnd.2	|- ( ph -> B e. V )
3		elmapsnd.3	|- ( ph -> ( F ` A ) e. B )
4		elsni	|- ( x e. { A } -> x = A )
5	4	fveq2d	|- ( x e. { A } -> ( F ` x ) = ( F ` A ) )
6	5	adantl	|- ( ( ph /\ x e. { A } ) -> ( F ` x ) = ( F ` A ) )
7	3	adantr	|- ( ( ph /\ x e. { A } ) -> ( F ` A ) e. B )
8	6 7	eqeltrd	|- ( ( ph /\ x e. { A } ) -> ( F ` x ) e. B )
9	8	ralrimiva	|- ( ph -> A. x e. { A } ( F ` x ) e. B )
10	1 9	jca	|- ( ph -> ( F Fn { A } /\ A. x e. { A } ( F ` x ) e. B ) )
11		ffnfv	|- ( F : { A } --> B <-> ( F Fn { A } /\ A. x e. { A } ( F ` x ) e. B ) )
12	10 11	sylibr	|- ( ph -> F : { A } --> B )
13		snex	|- { A } e. _V
14	13	a1i	|- ( ph -> { A } e. _V )
15	2 14	elmapd	|- ( ph -> ( F e. ( B ^m { A } ) <-> F : { A } --> B ) )
16	12 15	mpbird	|- ( ph -> F e. ( B ^m { A } ) )