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=\mathrm{Slot}N$$
	strfvi.x	$$⊢X=E\left(S\right)$$
Assertion	strfvi	$$⊢X=E\left(\mathrm{I}\left(S\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		strfvi.e	$$⊢E=\mathrm{Slot}N$$
2		strfvi.x	$$⊢X=E\left(S\right)$$
3		fvi	$$⊢S\in \mathrm{V}\to \mathrm{I}\left(S\right)=S$$
4	3	eqcomd	$$⊢S\in \mathrm{V}\to S=\mathrm{I}\left(S\right)$$
5	4	fveq2d	$$⊢S\in \mathrm{V}\to E\left(S\right)=E\left(\mathrm{I}\left(S\right)\right)$$
6	1	str0	$$⊢\varnothing =E\left(\varnothing \right)$$
7		fvprc	$$⊢\neg S\in \mathrm{V}\to E\left(S\right)=\varnothing$$
8		fvprc	$$⊢\neg S\in \mathrm{V}\to \mathrm{I}\left(S\right)=\varnothing$$
9	8	fveq2d	$$⊢\neg S\in \mathrm{V}\to E\left(\mathrm{I}\left(S\right)\right)=E\left(\varnothing \right)$$
10	6 7 9	3eqtr4a	$$⊢\neg S\in \mathrm{V}\to E\left(S\right)=E\left(\mathrm{I}\left(S\right)\right)$$
11	5 10	pm2.61i	$$⊢E\left(S\right)=E\left(\mathrm{I}\left(S\right)\right)$$
12	2 11	eqtri	$$⊢X=E\left(\mathrm{I}\left(S\right)\right)$$