Theorem funsseq

Description: Given two functions with equal domains, equality only requires one direction of the subset relationship. (Contributed by Scott Fenton, 24-Apr-2012) (Proof shortened by Mario Carneiro, 3-May-2015)

	Ref	Expression
Assertion	funsseq	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺 ) → ( 𝐹 = 𝐺 ↔ 𝐹 ⊆ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		eqimss	⊢ ( 𝐹 = 𝐺 → 𝐹 ⊆ 𝐺 )
2		simpl3	⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺 ) ∧ 𝐹 ⊆ 𝐺 ) → dom 𝐹 = dom 𝐺 )
3	2	reseq2d	⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺 ) ∧ 𝐹 ⊆ 𝐺 ) → ( 𝐺 ↾ dom 𝐹 ) = ( 𝐺 ↾ dom 𝐺 ) )
4		funssres	⊢ ( ( Fun 𝐺 ∧ 𝐹 ⊆ 𝐺 ) → ( 𝐺 ↾ dom 𝐹 ) = 𝐹 )
5	4	3ad2antl2	⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺 ) ∧ 𝐹 ⊆ 𝐺 ) → ( 𝐺 ↾ dom 𝐹 ) = 𝐹 )
6		simpl2	⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺 ) ∧ 𝐹 ⊆ 𝐺 ) → Fun 𝐺 )
7		funrel	⊢ ( Fun 𝐺 → Rel 𝐺 )
8		resdm	⊢ ( Rel 𝐺 → ( 𝐺 ↾ dom 𝐺 ) = 𝐺 )
9	6 7 8	3syl	⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺 ) ∧ 𝐹 ⊆ 𝐺 ) → ( 𝐺 ↾ dom 𝐺 ) = 𝐺 )
10	3 5 9	3eqtr3d	⊢ ( ( ( Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺 ) ∧ 𝐹 ⊆ 𝐺 ) → 𝐹 = 𝐺 )
11	10	ex	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺 ) → ( 𝐹 ⊆ 𝐺 → 𝐹 = 𝐺 ) )
12	1 11	impbid2	⊢ ( ( Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺 ) → ( 𝐹 = 𝐺 ↔ 𝐹 ⊆ 𝐺 ) )