Theorem fconst7

Description: An alternative way to express a constant function. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	fconst7.p	|- F/ x ph
	fconst7.x	|- F/_ x F
	fconst7.f	|- ( ph -> F Fn A )
	fconst7.b	|- ( ph -> B e. V )
	fconst7.e	|- ( ( ph /\ x e. A ) -> ( F ` x ) = B )
Assertion	fconst7	|- ( ph -> F = ( A X. { B } ) )

Proof

Step	Hyp	Ref	Expression
1		fconst7.p	|- F/ x ph
2		fconst7.x	|- F/_ x F
3		fconst7.f	|- ( ph -> F Fn A )
4		fconst7.b	|- ( ph -> B e. V )
5		fconst7.e	|- ( ( ph /\ x e. A ) -> ( F ` x ) = B )
6		fvexd	|- ( ( ph /\ x e. A ) -> ( F ` x ) e. _V )
7	5 6	eqeltrrd	|- ( ( ph /\ x e. A ) -> B e. _V )
8		snidg	|- ( B e. _V -> B e. { B } )
9	7 8	syl	|- ( ( ph /\ x e. A ) -> B e. { B } )
10	5 9	eqeltrd	|- ( ( ph /\ x e. A ) -> ( F ` x ) e. { B } )
11	1 10	ralrimia	|- ( ph -> A. x e. A ( F ` x ) e. { B } )
12		nfcv	|- F/_ x A
13		nfcv	|- F/_ x { B }
14	12 13 2	ffnfvf	|- ( F : A --> { B } <-> ( F Fn A /\ A. x e. A ( F ` x ) e. { B } ) )
15	3 11 14	sylanbrc	|- ( ph -> F : A --> { B } )
16		fconst2g	|- ( B e. V -> ( F : A --> { B } <-> F = ( A X. { B } ) ) )
17	4 16	syl	|- ( ph -> ( F : A --> { B } <-> F = ( A X. { B } ) ) )
18	15 17	mpbid	|- ( ph -> F = ( A X. { B } ) )