Theorem f1sn2g

Description: A function that maps a singleton to a class is injective. (Contributed by Zhi Wang, 1-Oct-2024)

	Ref	Expression
Assertion	f1sn2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : { 𝐴 } ⟶ 𝐵 ) → 𝐹 : { 𝐴 } –1-1→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fsn2g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐹 : { 𝐴 } ⟶ 𝐵 ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) ) )
2	1	biimpa	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : { 𝐴 } ⟶ 𝐵 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ∧ 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } ) )
3	2	simpld	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : { 𝐴 } ⟶ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 )
4		f1sng	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } : { 𝐴 } –1-1→ 𝐵 )
5	3 4	syldan	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : { 𝐴 } ⟶ 𝐵 ) → { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } : { 𝐴 } –1-1→ 𝐵 )
6		f1eq1	⊢ ( 𝐹 = { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } → ( 𝐹 : { 𝐴 } –1-1→ 𝐵 ↔ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } : { 𝐴 } –1-1→ 𝐵 ) )
7	2 6	simpl2im	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : { 𝐴 } ⟶ 𝐵 ) → ( 𝐹 : { 𝐴 } –1-1→ 𝐵 ↔ { ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ } : { 𝐴 } –1-1→ 𝐵 ) )
8	5 7	mpbird	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 : { 𝐴 } ⟶ 𝐵 ) → 𝐹 : { 𝐴 } –1-1→ 𝐵 )