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 ) ) )