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 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
fsneq.b ⊢ 𝐵 = { 𝐴 }
fsneq.f ⊢ ( 𝜑 → 𝐹 Fn 𝐵 )
fsneq.g ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
Assertion fsneq ( 𝜑 → ( 𝐹 = 𝐺 ↔ ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 fsneq.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 fsneq.b ⊢ 𝐵 = { 𝐴 }
3 fsneq.f ⊢ ( 𝜑 → 𝐹 Fn 𝐵 )
4 fsneq.g ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
5 eqfnfv ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐺 Fn 𝐵 ) → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
6 3 4 5 syl2anc ⊢ ( 𝜑 → ( 𝐹 = 𝐺 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
7 snidg ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
8 1 7 syl ⊢ ( 𝜑 → 𝐴 ∈ { 𝐴 } )
9 2 eqcomi ⊢ { 𝐴 } = 𝐵
10 9 a1i ⊢ ( 𝜑 → { 𝐴 } = 𝐵 )
11 8 10 eleqtrd ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
12 11 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) → 𝐴 ∈ 𝐵 )
13 simpr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
14 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
15 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝐴 ) )
16 14 15 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ) )
17 16 rspcva ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) )
18 12 13 17 syl2anc ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) )
19 18 ex ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ) )
20 simpl ⊢ ( ( ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) )
21 2 eleq2i ⊢ ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ { 𝐴 } )
22 21 biimpi ⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ { 𝐴 } )
23 velsn ⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
24 22 23 sylib ⊢ ( 𝑥 ∈ 𝐵 → 𝑥 = 𝐴 )
25 24 fveq2d ⊢ ( 𝑥 ∈ 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
26 25 adantl ⊢ ( ( ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
27 24 fveq2d ⊢ ( 𝑥 ∈ 𝐵 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝐴 ) )
28 27 adantl ⊢ ( ( ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝐴 ) )
29 20 26 28 3eqtr4d ⊢ ( ( ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
30 29 adantll ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
31 30 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
32 31 ex ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) → ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
33 19 32 impbid ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ) )
34 6 33 bitrd ⊢ ( 𝜑 → ( 𝐹 = 𝐺 ↔ ( 𝐹 ‘ 𝐴 ) = ( 𝐺 ‘ 𝐴 ) ) )