Theorem strfv2

Description: A variation on strfv to avoid asserting that S itself is a function, which involves sethood of all the ordered pair components of S . (Contributed by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypotheses	strfv2.s	|- S e. _V
	strfv2.f	|- Fun `' `' S
	strfv2.e	|- E = Slot ( E ` ndx )
	strfv2.n	|- <. ( E ` ndx ) , C >. e. S
Assertion	strfv2	|- ( C e. V -> C = ( E ` S ) )

Proof

Step	Hyp	Ref	Expression
1		strfv2.s	|- S e. _V
2		strfv2.f	|- Fun `' `' S
3		strfv2.e	|- E = Slot ( E ` ndx )
4		strfv2.n	|- <. ( E ` ndx ) , C >. e. S
5	1	a1i	|- ( C e. V -> S e. _V )
6	2	a1i	|- ( C e. V -> Fun `' `' S )
7	4	a1i	|- ( C e. V -> <. ( E ` ndx ) , C >. e. S )
8		id	|- ( C e. V -> C e. V )
9	3 5 6 7 8	strfv2d	|- ( C e. V -> C = ( E ` S ) )