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	⊢ 𝐸 = Slot 𝑁
	strfvi.x	⊢ 𝑋 = ( 𝐸 ‘ 𝑆 )
Assertion	strfvi	⊢ 𝑋 = ( 𝐸 ‘ ( I ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		strfvi.e	⊢ 𝐸 = Slot 𝑁
2		strfvi.x	⊢ 𝑋 = ( 𝐸 ‘ 𝑆 )
3		fvi	⊢ ( 𝑆 ∈ V → ( I ‘ 𝑆 ) = 𝑆 )
4	3	eqcomd	⊢ ( 𝑆 ∈ V → 𝑆 = ( I ‘ 𝑆 ) )
5	4	fveq2d	⊢ ( 𝑆 ∈ V → ( 𝐸 ‘ 𝑆 ) = ( 𝐸 ‘ ( I ‘ 𝑆 ) ) )
6	1	str0	⊢ ∅ = ( 𝐸 ‘ ∅ )
7		fvprc	⊢ ( ¬ 𝑆 ∈ V → ( 𝐸 ‘ 𝑆 ) = ∅ )
8		fvprc	⊢ ( ¬ 𝑆 ∈ V → ( I ‘ 𝑆 ) = ∅ )
9	8	fveq2d	⊢ ( ¬ 𝑆 ∈ V → ( 𝐸 ‘ ( I ‘ 𝑆 ) ) = ( 𝐸 ‘ ∅ ) )
10	6 7 9	3eqtr4a	⊢ ( ¬ 𝑆 ∈ V → ( 𝐸 ‘ 𝑆 ) = ( 𝐸 ‘ ( I ‘ 𝑆 ) ) )
11	5 10	pm2.61i	⊢ ( 𝐸 ‘ 𝑆 ) = ( 𝐸 ‘ ( I ‘ 𝑆 ) )
12	2 11	eqtri	⊢ 𝑋 = ( 𝐸 ‘ ( I ‘ 𝑆 ) )