Theorem fsneq

Description: Equality condition for two functions defined on a singleton. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	fsneq.a	$$⊢\phi \to A\in V$$
	fsneq.b	$$⊢B=\left\{A\right\}$$
	fsneq.f	$$⊢\phi \to FFnB$$
	fsneq.g	$$⊢\phi \to GFnB$$
Assertion	fsneq	$$⊢\phi \to \left(F=G\leftrightarrow F\left(A\right)=G\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsneq.a	$$⊢\phi \to A\in V$$
2		fsneq.b	$$⊢B=\left\{A\right\}$$
3		fsneq.f	$$⊢\phi \to FFnB$$
4		fsneq.g	$$⊢\phi \to GFnB$$
5		eqfnfv	$$⊢\left(FFnB\wedge GFnB\right)\to \left(F=G\leftrightarrow \forall x\in BF\left(x\right)=G\left(x\right)\right)$$
6	3 4 5	syl2anc	$$⊢\phi \to \left(F=G\leftrightarrow \forall x\in BF\left(x\right)=G\left(x\right)\right)$$
7		snidg	$$⊢A\in V\to A\in \left\{A\right\}$$
8	1 7	syl	$$⊢\phi \to A\in \left\{A\right\}$$
9	2	eqcomi	$$⊢\left\{A\right\}=B$$
10	9	a1i	$$⊢\phi \to \left\{A\right\}=B$$
11	8 10	eleqtrd	$$⊢\phi \to A\in B$$
12	11	adantr	$$⊢\left(\phi \wedge \forall x\in BF\left(x\right)=G\left(x\right)\right)\to A\in B$$
13		simpr	$$⊢\left(\phi \wedge \forall x\in BF\left(x\right)=G\left(x\right)\right)\to \forall x\in BF\left(x\right)=G\left(x\right)$$
14		fveq2	$$⊢x=A\to F\left(x\right)=F\left(A\right)$$
15		fveq2	$$⊢x=A\to G\left(x\right)=G\left(A\right)$$
16	14 15	eqeq12d	$$⊢x=A\to \left(F\left(x\right)=G\left(x\right)\leftrightarrow F\left(A\right)=G\left(A\right)\right)$$
17	16	rspcva	$$⊢\left(A\in B\wedge \forall x\in BF\left(x\right)=G\left(x\right)\right)\to F\left(A\right)=G\left(A\right)$$
18	12 13 17	syl2anc	$$⊢\left(\phi \wedge \forall x\in BF\left(x\right)=G\left(x\right)\right)\to F\left(A\right)=G\left(A\right)$$
19	18	ex	$$⊢\phi \to \left(\forall x\in BF\left(x\right)=G\left(x\right)\to F\left(A\right)=G\left(A\right)\right)$$
20		simpl	$$⊢\left(F\left(A\right)=G\left(A\right)\wedge x\in B\right)\to F\left(A\right)=G\left(A\right)$$
21	2	eleq2i	$$⊢x\in B\leftrightarrow x\in \left\{A\right\}$$
22	21	biimpi	$$⊢x\in B\to x\in \left\{A\right\}$$
23		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
24	22 23	sylib	$$⊢x\in B\to x=A$$
25	24	fveq2d	$$⊢x\in B\to F\left(x\right)=F\left(A\right)$$
26	25	adantl	$$⊢\left(F\left(A\right)=G\left(A\right)\wedge x\in B\right)\to F\left(x\right)=F\left(A\right)$$
27	24	fveq2d	$$⊢x\in B\to G\left(x\right)=G\left(A\right)$$
28	27	adantl	$$⊢\left(F\left(A\right)=G\left(A\right)\wedge x\in B\right)\to G\left(x\right)=G\left(A\right)$$
29	20 26 28	3eqtr4d	$$⊢\left(F\left(A\right)=G\left(A\right)\wedge x\in B\right)\to F\left(x\right)=G\left(x\right)$$
30	29	adantll	$$⊢\left(\left(\phi \wedge F\left(A\right)=G\left(A\right)\right)\wedge x\in B\right)\to F\left(x\right)=G\left(x\right)$$
31	30	ralrimiva	$$⊢\left(\phi \wedge F\left(A\right)=G\left(A\right)\right)\to \forall x\in BF\left(x\right)=G\left(x\right)$$
32	31	ex	$$⊢\phi \to \left(F\left(A\right)=G\left(A\right)\to \forall x\in BF\left(x\right)=G\left(x\right)\right)$$
33	19 32	impbid	$$⊢\phi \to \left(\forall x\in BF\left(x\right)=G\left(x\right)\leftrightarrow F\left(A\right)=G\left(A\right)\right)$$
34	6 33	bitrd	$$⊢\phi \to \left(F=G\leftrightarrow F\left(A\right)=G\left(A\right)\right)$$