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 >. | ( ph /\ y = A ) }

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( ph /\ y = A ) -> y = A )
2	1	ssopab2i	|- { <. x , y >. | ( ph /\ y = A ) } C_ { <. x , y >. | y = A }
3		funopabeq	|- Fun { <. x , y >. | y = A }
4		funss	|- ( { <. x , y >. | ( ph /\ y = A ) } C_ { <. x , y >. | y = A } -> ( Fun { <. x , y >. | y = A } -> Fun { <. x , y >. | ( ph /\ y = A ) } ) )
5	2 3 4	mp2	|- Fun { <. x , y >. | ( ph /\ y = A ) }