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 ⊢ 𝐸 = 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 ‘ 𝑆 ) )