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 \in V \to I (S) = S$
4	3	eqcomd	$⊢ S \in V \to S = I (S)$
5	4	fveq2d	$⊢ S \in V \to E (S) = E (I (S))$
6	1	str0	$⊢ \emptyset = E (\emptyset)$
7		fvprc	$⊢ \neg S \in V \to E (S) = \emptyset$
8		fvprc	$⊢ \neg S \in V \to I (S) = \emptyset$
9	8	fveq2d	$⊢ \neg S \in V \to E (I (S)) = E (\emptyset)$
10	6 7 9	3eqtr4a	$⊢ \neg S \in V \to E (S) = E (I (S))$
11	5 10	pm2.61i	$⊢ E (S) = E (I (S))$
12	2 11	eqtri	$⊢ X = E (I (S))$

Metamath Proof Explorer

Theorem strfvi

Proof