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

Metamath Proof Explorer

Theorem strfvd

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

Ref Expression
Hypotheses strfvd.e ⊢ E = Slot E ⁡ ndx
strfvd.s ⊢ φ → S ∈ V
strfvd.f ⊢ φ → Fun ⁡ S
strfvd.n ⊢ φ → E ⁡ ndx C ∈ S
Assertion strfvd ⊢ φ → C = E ⁡ S

Proof

Step Hyp Ref Expression
1 strfvd.e ⊢ E = Slot E ⁡ ndx
2 strfvd.s ⊢ φ → S ∈ V
3 strfvd.f ⊢ φ → Fun ⁡ S
4 strfvd.n ⊢ φ → E ⁡ ndx C ∈ S
5 1 2 strfvnd ⊢ φ → E ⁡ S = S ⁡ E ⁡ ndx
6 funopfv ⊢ Fun ⁡ S → E ⁡ ndx C ∈ S → S ⁡ E ⁡ ndx = C
7 3 4 6 sylc ⊢ φ → S ⁡ E ⁡ ndx = C
8 5 7 eqtr2d ⊢ φ → C = E ⁡ S