Metamath Proof Explorer

Theorem funbreq

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

	Ref	Expression
Hypotheses	funbreq.1	$⊢ A \in V$
	funbreq.2	$⊢ B \in V$
	funbreq.3	$⊢ C \in V$
Assertion	funbreq	$⊢ (Fun F \land A F B) \to (A F C \leftrightarrow B = C)$

Step	Hyp	Ref	Expression
1		funbreq.1	$⊢ A \in V$
2		funbreq.2	$⊢ B \in V$
3		funbreq.3	$⊢ C \in V$
4	1 2 3	fununiq	$⊢ Fun F \to ((A F B \land A F C) \to B = C)$
5	4	expdimp	$⊢ (Fun F \land A F B) \to (A F C \to B = C)$
6		breq2	$⊢ B = C \to (A F B \leftrightarrow A F C)$
7	6	biimpcd	$⊢ A F B \to (B = C \to A F C)$
8	7	adantl	$⊢ (Fun F \land A F B) \to (B = C \to A F C)$
9	5 8	impbid	$⊢ (Fun F \land A F B) \to (A F C \leftrightarrow B = C)$