Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cntzval Structured version   Visualization version   Unicode version

Theorem cntzval 17053
 Description: Definition substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.)
Hypotheses
Ref Expression
cntzfval.b
cntzfval.p
cntzfval.z Cntz
Assertion
Ref Expression
cntzval
Distinct variable groups:   ,,   ,   ,,   ,,
Allowed substitution hints:   ()   (,)

Proof of Theorem cntzval
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 cntzfval.b . . . . 5
2 cntzfval.p . . . . 5
3 cntzfval.z . . . . 5 Cntz
41, 2, 3cntzfval 17052 . . . 4
54fveq1d 5881 . . 3
6 fvex 5889 . . . . . 6
71, 6eqeltri 2545 . . . . 5
87elpw2 4565 . . . 4
9 raleq 2973 . . . . . 6
109rabbidv 3022 . . . . 5
11 eqid 2471 . . . . 5
127rabex 4550 . . . . 5
1310, 11, 12fvmpt 5963 . . . 4
148, 13sylbir 218 . . 3
155, 14sylan9eq 2525 . 2
16 0fv 5912 . . . 4
17 fvprc 5873 . . . . . 6 Cntz
183, 17syl5eq 2517 . . . . 5
1918fveq1d 5881 . . . 4
20 ssrab2 3500 . . . . . 6
21 fvprc 5873 . . . . . . 7
221, 21syl5eq 2517 . . . . . 6
2320, 22syl5sseq 3466 . . . . 5
24 ss0 3768 . . . . 5
2523, 24syl 17 . . . 4
2616, 19, 253eqtr4a 2531 . . 3