Theorem strfv2

Description: A variation on strfv to avoid asserting that S itself is a function, which involves sethood of all the ordered pair components of S . (Contributed by Mario Carneiro, 30-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		strfv2.s	$$⊢S\in \mathrm{V}$$
2		strfv2.f	$$⊢\mathrm{Fun}{S^{-1}}^{-1}$$
3		strfv2.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
4		strfv2.n	$$⊢⟨E\left(\mathrm{ndx}\right),C⟩\in S$$
5	1	a1i	$$⊢C\in V\to S\in \mathrm{V}$$
6	2	a1i	$$⊢C\in V\to \mathrm{Fun}{S^{-1}}^{-1}$$
7	4	a1i	$$⊢C\in V\to ⟨E\left(\mathrm{ndx}\right),C⟩\in S$$
8		id	$$⊢C\in V\to C\in V$$
9	3 5 6 7 8	strfv2d	$$⊢C\in V\to C=E\left(S\right)$$