This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funeqd

Description: Equality deduction for the function predicate. (Contributed by NM, 23-Feb-2013)

		Ref	Expression
	Hypothesis	funeqd.1	$⊢ φ \to A = B$
	Assertion	funeqd	$⊢ φ \to (Fun A \leftrightarrow Fun B)$

Step	Hyp	Ref	Expression
1		funeqd.1	$⊢ φ \to A = B$
2		funeq	$⊢ A = B \to (Fun A \leftrightarrow Fun B)$
3	1 2	syl	$⊢ φ \to (Fun A \leftrightarrow Fun B)$