This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ V
strfv2.f ⊢ Fun ⁡ S -1 -1
strfv2.e ⊢ E = Slot E ⁡ ndx
strfv2.n ⊢ E ⁡ ndx C ∈ S
Assertion strfv2 ⊢ C ∈ V → C = E ⁡ S

Proof

Step Hyp Ref Expression
1 strfv2.s ⊢ S ∈ V
2 strfv2.f ⊢ Fun ⁡ S -1 -1
3 strfv2.e ⊢ E = Slot E ⁡ ndx
4 strfv2.n ⊢ E ⁡ ndx C ∈ S
5 1 a1i ⊢ C ∈ V → S ∈ V
6 2 a1i ⊢ C ∈ V → Fun ⁡ S -1 -1
7 4 a1i ⊢ C ∈ V → E ⁡ ndx C ∈ S
8 id ⊢ C ∈ V → C ∈ V
9 3 5 6 7 8 strfv2d ⊢ C ∈ V → C = E ⁡ S