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

Metamath Proof Explorer

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 ) )