Theorem fvopab4ndm

Description: Value of a function given by an ordered-pair class abstraction, outside of its domain. (Contributed by NM, 28-Mar-2008)

	Ref	Expression
Hypothesis	fvopab4ndm.1	|- F = { <. x , y >. | ( x e. A /\ ph ) }
Assertion	fvopab4ndm	|- ( -. B e. A -> ( F ` B ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		fvopab4ndm.1	|- F = { <. x , y >. | ( x e. A /\ ph ) }
2	1	dmeqi	|- dom F = dom { <. x , y >. | ( x e. A /\ ph ) }
3		dmopabss	|- dom { <. x , y >. | ( x e. A /\ ph ) } C_ A
4	2 3	eqsstri	|- dom F C_ A
5	4	sseli	|- ( B e. dom F -> B e. A )
6		ndmfv	|- ( -. B e. dom F -> ( F ` B ) = (/) )
7	5 6	nsyl5	|- ( -. B e. A -> ( F ` B ) = (/) )