Theorem strfvd

Description: Deduction version of strfv . (Contributed by Mario Carneiro, 15-Nov-2014)

	Ref	Expression
Hypotheses	strfvd.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
	strfvd.s	$$⊢\phi \to S\in V$$
	strfvd.f	$$⊢\phi \to \mathrm{Fun}S$$
	strfvd.n	$$⊢\phi \to ⟨E\left(\mathrm{ndx}\right),C⟩\in S$$
Assertion	strfvd	$$⊢\phi \to C=E\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		strfvd.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
2		strfvd.s	$$⊢\phi \to S\in V$$
3		strfvd.f	$$⊢\phi \to \mathrm{Fun}S$$
4		strfvd.n	$$⊢\phi \to ⟨E\left(\mathrm{ndx}\right),C⟩\in S$$
5	1 2	strfvnd	$$⊢\phi \to E\left(S\right)=S\left(E\left(\mathrm{ndx}\right)\right)$$
6		funopfv	$$⊢\mathrm{Fun}S\to \left(⟨E\left(\mathrm{ndx}\right),C⟩\in S\to S\left(E\left(\mathrm{ndx}\right)\right)=C\right)$$
7	3 4 6	sylc	$$⊢\phi \to S\left(E\left(\mathrm{ndx}\right)\right)=C$$
8	5 7	eqtr2d	$$⊢\phi \to C=E\left(S\right)$$