Metamath Proof Explorer


Theorem fsneq

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

Ref Expression
Hypotheses fsneq.a
|- ( ph -> A e. V )
fsneq.b
|- B = { A }
fsneq.f
|- ( ph -> F Fn B )
fsneq.g
|- ( ph -> G Fn B )
Assertion fsneq
|- ( ph -> ( F = G <-> ( F ` A ) = ( G ` A ) ) )

Proof

Step Hyp Ref Expression
1 fsneq.a
 |-  ( ph -> A e. V )
2 fsneq.b
 |-  B = { A }
3 fsneq.f
 |-  ( ph -> F Fn B )
4 fsneq.g
 |-  ( ph -> G Fn B )
5 eqfnfv
 |-  ( ( F Fn B /\ G Fn B ) -> ( F = G <-> A. x e. B ( F ` x ) = ( G ` x ) ) )
6 3 4 5 syl2anc
 |-  ( ph -> ( F = G <-> A. x e. B ( F ` x ) = ( G ` x ) ) )
7 snidg
 |-  ( A e. V -> A e. { A } )
8 1 7 syl
 |-  ( ph -> A e. { A } )
9 2 eqcomi
 |-  { A } = B
10 9 a1i
 |-  ( ph -> { A } = B )
11 8 10 eleqtrd
 |-  ( ph -> A e. B )
12 11 adantr
 |-  ( ( ph /\ A. x e. B ( F ` x ) = ( G ` x ) ) -> A e. B )
13 simpr
 |-  ( ( ph /\ A. x e. B ( F ` x ) = ( G ` x ) ) -> A. x e. B ( F ` x ) = ( G ` x ) )
14 fveq2
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
15 fveq2
 |-  ( x = A -> ( G ` x ) = ( G ` A ) )
16 14 15 eqeq12d
 |-  ( x = A -> ( ( F ` x ) = ( G ` x ) <-> ( F ` A ) = ( G ` A ) ) )
17 16 rspcva
 |-  ( ( A e. B /\ A. x e. B ( F ` x ) = ( G ` x ) ) -> ( F ` A ) = ( G ` A ) )
18 12 13 17 syl2anc
 |-  ( ( ph /\ A. x e. B ( F ` x ) = ( G ` x ) ) -> ( F ` A ) = ( G ` A ) )
19 18 ex
 |-  ( ph -> ( A. x e. B ( F ` x ) = ( G ` x ) -> ( F ` A ) = ( G ` A ) ) )
20 simpl
 |-  ( ( ( F ` A ) = ( G ` A ) /\ x e. B ) -> ( F ` A ) = ( G ` A ) )
21 2 eleq2i
 |-  ( x e. B <-> x e. { A } )
22 21 biimpi
 |-  ( x e. B -> x e. { A } )
23 velsn
 |-  ( x e. { A } <-> x = A )
24 22 23 sylib
 |-  ( x e. B -> x = A )
25 24 fveq2d
 |-  ( x e. B -> ( F ` x ) = ( F ` A ) )
26 25 adantl
 |-  ( ( ( F ` A ) = ( G ` A ) /\ x e. B ) -> ( F ` x ) = ( F ` A ) )
27 24 fveq2d
 |-  ( x e. B -> ( G ` x ) = ( G ` A ) )
28 27 adantl
 |-  ( ( ( F ` A ) = ( G ` A ) /\ x e. B ) -> ( G ` x ) = ( G ` A ) )
29 20 26 28 3eqtr4d
 |-  ( ( ( F ` A ) = ( G ` A ) /\ x e. B ) -> ( F ` x ) = ( G ` x ) )
30 29 adantll
 |-  ( ( ( ph /\ ( F ` A ) = ( G ` A ) ) /\ x e. B ) -> ( F ` x ) = ( G ` x ) )
31 30 ralrimiva
 |-  ( ( ph /\ ( F ` A ) = ( G ` A ) ) -> A. x e. B ( F ` x ) = ( G ` x ) )
32 31 ex
 |-  ( ph -> ( ( F ` A ) = ( G ` A ) -> A. x e. B ( F ` x ) = ( G ` x ) ) )
33 19 32 impbid
 |-  ( ph -> ( A. x e. B ( F ` x ) = ( G ` x ) <-> ( F ` A ) = ( G ` A ) ) )
34 6 33 bitrd
 |-  ( ph -> ( F = G <-> ( F ` A ) = ( G ` A ) ) )