Theorem strfvi

Description: Structure slot extractors cannot distinguish between proper classes and (/) , so they can be protected using the identity function. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypotheses	strfvi.e	|- E = Slot N
	strfvi.x	|- X = ( E ` S )
Assertion	strfvi	|- X = ( E ` ( _I ` S ) )

Proof

Step	Hyp	Ref	Expression
1		strfvi.e	|- E = Slot N
2		strfvi.x	|- X = ( E ` S )
3		fvi	|- ( S e. _V -> ( _I ` S ) = S )
4	3	eqcomd	|- ( S e. _V -> S = ( _I ` S ) )
5	4	fveq2d	|- ( S e. _V -> ( E ` S ) = ( E ` ( _I ` S ) ) )
6	1	str0	|- (/) = ( E ` (/) )
7		fvprc	|- ( -. S e. _V -> ( E ` S ) = (/) )
8		fvprc	|- ( -. S e. _V -> ( _I ` S ) = (/) )
9	8	fveq2d	|- ( -. S e. _V -> ( E ` ( _I ` S ) ) = ( E ` (/) ) )
10	6 7 9	3eqtr4a	|- ( -. S e. _V -> ( E ` S ) = ( E ` ( _I ` S ) ) )
11	5 10	pm2.61i	|- ( E ` S ) = ( E ` ( _I ` S ) )
12	2 11	eqtri	|- X = ( E ` ( _I ` S ) )