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

Metamath Proof Explorer

Theorem funopab4

Description: A class of ordered pairs of values in the form used by df-mpt is a function. (Contributed by NM, 17-Feb-2013)

		Ref	Expression
	Assertion	funopab4	$⊢ Fun \{⟨x, y⟩ \| (φ \land y = A)\}$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (φ \land y = A) \to y = A$
2	1	ssopab2i	$⊢ \{⟨x, y⟩ \| (φ \land y = A)\} \subseteq \{⟨x, y⟩ \| y = A\}$
3		funopabeq	$⊢ Fun \{⟨x, y⟩ \| y = A\}$
4		funss	$⊢ \{⟨x, y⟩ \| (φ \land y = A)\} \subseteq \{⟨x, y⟩ \| y = A\} \to (Fun \{⟨x, y⟩ \| y = A\} \to Fun \{⟨x, y⟩ \| (φ \land y = A)\})$
5	2 3 4	mp2	$⊢ Fun \{⟨x, y⟩ \| (φ \land y = A)\}$