# 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}=\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 ${⊢}¬{S}\in \mathrm{V}\to {E}\left({S}\right)=\varnothing$
8 fvprc ${⊢}¬{S}\in \mathrm{V}\to \mathrm{I}\left({S}\right)=\varnothing$
9 8 fveq2d ${⊢}¬{S}\in \mathrm{V}\to {E}\left(\mathrm{I}\left({S}\right)\right)={E}\left(\varnothing \right)$
10 6 7 9 3eqtr4a ${⊢}¬{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)$