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 F /\ Fun G /\ dom F = dom G ) -> ( F = G <-> F C_ G ) )

Proof

Step	Hyp	Ref	Expression
1		eqimss	|- ( F = G -> F C_ G )
2		simpl3	|- ( ( ( Fun F /\ Fun G /\ dom F = dom G ) /\ F C_ G ) -> dom F = dom G )
3	2	reseq2d	|- ( ( ( Fun F /\ Fun G /\ dom F = dom G ) /\ F C_ G ) -> ( G |` dom F ) = ( G |` dom G ) )
4		funssres	|- ( ( Fun G /\ F C_ G ) -> ( G |` dom F ) = F )
5	4	3ad2antl2	|- ( ( ( Fun F /\ Fun G /\ dom F = dom G ) /\ F C_ G ) -> ( G |` dom F ) = F )
6		simpl2	|- ( ( ( Fun F /\ Fun G /\ dom F = dom G ) /\ F C_ G ) -> Fun G )
7		funrel	|- ( Fun G -> Rel G )
8		resdm	|- ( Rel G -> ( G |` dom G ) = G )
9	6 7 8	3syl	|- ( ( ( Fun F /\ Fun G /\ dom F = dom G ) /\ F C_ G ) -> ( G |` dom G ) = G )
10	3 5 9	3eqtr3d	|- ( ( ( Fun F /\ Fun G /\ dom F = dom G ) /\ F C_ G ) -> F = G )
11	10	ex	|- ( ( Fun F /\ Fun G /\ dom F = dom G ) -> ( F C_ G -> F = G ) )
12	1 11	impbid2	|- ( ( Fun F /\ Fun G /\ dom F = dom G ) -> ( F = G <-> F C_ G ) )