Theorem f1ssf1

Description: A subset of an injective function is injective. (Contributed by AV, 20-Nov-2020)

	Ref	Expression
Assertion	f1ssf1	⊢ ( ( Fun 𝐹 ∧ Fun ◡ 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → Fun ◡ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		funssres	⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( 𝐹 ↾ dom 𝐺 ) = 𝐺 )
2		funres11	⊢ ( Fun ◡ 𝐹 → Fun ◡ ( 𝐹 ↾ dom 𝐺 ) )
3		cnveq	⊢ ( 𝐺 = ( 𝐹 ↾ dom 𝐺 ) → ◡ 𝐺 = ◡ ( 𝐹 ↾ dom 𝐺 ) )
4	3	funeqd	⊢ ( 𝐺 = ( 𝐹 ↾ dom 𝐺 ) → ( Fun ◡ 𝐺 ↔ Fun ◡ ( 𝐹 ↾ dom 𝐺 ) ) )
5	2 4	imbitrrid	⊢ ( 𝐺 = ( 𝐹 ↾ dom 𝐺 ) → ( Fun ◡ 𝐹 → Fun ◡ 𝐺 ) )
6	5	eqcoms	⊢ ( ( 𝐹 ↾ dom 𝐺 ) = 𝐺 → ( Fun ◡ 𝐹 → Fun ◡ 𝐺 ) )
7	1 6	syl	⊢ ( ( Fun 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → ( Fun ◡ 𝐹 → Fun ◡ 𝐺 ) )
8	7	ex	⊢ ( Fun 𝐹 → ( 𝐺 ⊆ 𝐹 → ( Fun ◡ 𝐹 → Fun ◡ 𝐺 ) ) )
9	8	com23	⊢ ( Fun 𝐹 → ( Fun ◡ 𝐹 → ( 𝐺 ⊆ 𝐹 → Fun ◡ 𝐺 ) ) )
10	9	3imp	⊢ ( ( Fun 𝐹 ∧ Fun ◡ 𝐹 ∧ 𝐺 ⊆ 𝐹 ) → Fun ◡ 𝐺 )