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	⊢ 𝑆 ∈ V
	strfv2.f	⊢ Fun ◡ ◡ 𝑆
	strfv2.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
	strfv2.n	⊢ ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆
Assertion	strfv2	⊢ ( 𝐶 ∈ 𝑉 → 𝐶 = ( 𝐸 ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		strfv2.s	⊢ 𝑆 ∈ V
2		strfv2.f	⊢ Fun ◡ ◡ 𝑆
3		strfv2.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
4		strfv2.n	⊢ ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆
5	1	a1i	⊢ ( 𝐶 ∈ 𝑉 → 𝑆 ∈ V )
6	2	a1i	⊢ ( 𝐶 ∈ 𝑉 → Fun ◡ ◡ 𝑆 )
7	4	a1i	⊢ ( 𝐶 ∈ 𝑉 → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆 )
8		id	⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ 𝑉 )
9	3 5 6 7 8	strfv2d	⊢ ( 𝐶 ∈ 𝑉 → 𝐶 = ( 𝐸 ‘ 𝑆 ) )