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

Metamath Proof Explorer

Theorem fneq1i

Description: Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011)

		Ref	Expression
	Hypothesis	fneq1i.1	$⊢ F = G$
	Assertion	fneq1i	$⊢ F Fn A \leftrightarrow G Fn A$

Step	Hyp	Ref	Expression
1		fneq1i.1	$⊢ F = G$
2		fneq1	$⊢ F = G \to (F Fn A \leftrightarrow G Fn A)$
3	1 2	ax-mp	$⊢ F Fn A \leftrightarrow G Fn A$