Theorem funbreq

Description: An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013)

	Ref	Expression
Hypotheses	funbreq.1	|- A e. _V
	funbreq.2	|- B e. _V
	funbreq.3	|- C e. _V
Assertion	funbreq	|- ( ( Fun F /\ A F B ) -> ( A F C <-> B = C ) )

Proof

Step	Hyp	Ref	Expression
1		funbreq.1	|- A e. _V
2		funbreq.2	|- B e. _V
3		funbreq.3	|- C e. _V
4	1 2 3	fununiq	|- ( Fun F -> ( ( A F B /\ A F C ) -> B = C ) )
5	4	expdimp	|- ( ( Fun F /\ A F B ) -> ( A F C -> B = C ) )
6		breq2	|- ( B = C -> ( A F B <-> A F C ) )
7	6	biimpcd	|- ( A F B -> ( B = C -> A F C ) )
8	7	adantl	|- ( ( Fun F /\ A F B ) -> ( B = C -> A F C ) )
9	5 8	impbid	|- ( ( Fun F /\ A F B ) -> ( A F C <-> B = C ) )