Metamath Proof Explorer


Theorem strfv2d

Description: Deduction version of strfv2 . (Contributed by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses strfv2d.e E = Slot E ndx
strfv2d.s φ S V
strfv2d.f φ Fun S -1 -1
strfv2d.n φ E ndx C S
strfv2d.c φ C W
Assertion strfv2d φ C = E S

Proof

Step Hyp Ref Expression
1 strfv2d.e E = Slot E ndx
2 strfv2d.s φ S V
3 strfv2d.f φ Fun S -1 -1
4 strfv2d.n φ E ndx C S
5 strfv2d.c φ C W
6 1 2 strfvnd φ E S = S E ndx
7 cnvcnv2 S -1 -1 = S V
8 7 fveq1i S -1 -1 E ndx = S V E ndx
9 fvex E ndx V
10 fvres E ndx V S V E ndx = S E ndx
11 9 10 ax-mp S V E ndx = S E ndx
12 8 11 eqtri S -1 -1 E ndx = S E ndx
13 5 elexd φ C V
14 opelxpi E ndx V C V E ndx C V × V
15 9 13 14 sylancr φ E ndx C V × V
16 4 15 elind φ E ndx C S V × V
17 cnvcnv S -1 -1 = S V × V
18 16 17 eleqtrrdi φ E ndx C S -1 -1
19 funopfv Fun S -1 -1 E ndx C S -1 -1 S -1 -1 E ndx = C
20 3 18 19 sylc φ S -1 -1 E ndx = C
21 12 20 eqtr3id φ S E ndx = C
22 6 21 eqtr2d φ C = E S