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

Theorem cntzval 15120
 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 15119 . . . 4
54fveq1d 5730 . . 3
6 fvex 5742 . . . . . 6
71, 6eqeltri 2506 . . . . 5
87elpw2 4364 . . . 4
9 raleq 2904 . . . . . 6
109rabbidv 2948 . . . . 5
11 eqid 2436 . . . . 5
127rabex 4354 . . . . 5
1310, 11, 12fvmpt 5806 . . . 4
148, 13sylbir 205 . . 3
155, 14sylan9eq 2488 . 2
16 fv01 5763 . . . 4
17 fvprc 5722 . . . . . 6 Cntz
183, 17syl5eq 2480 . . . . 5
1918fveq1d 5730 . . . 4
20 ssrab2 3428 . . . . . 6
21 fvprc 5722 . . . . . . 7
221, 21syl5eq 2480 . . . . . 6
2320, 22syl5sseq 3396 . . . . 5
24 ss0 3658 . . . . 5
2523, 24syl 16 . . . 4
2616, 19, 253eqtr4a 2494 . . 3