Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cmtvalN Unicode version

Theorem cmtvalN 29848
 Description: Equivalence for commutes relation. Definition of commutes in [Kalmbach] p. 20. (cmbr 23074 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
cmtfval.b
cmtfval.j
cmtfval.m
cmtfval.o
cmtfval.c
Assertion
Ref Expression
cmtvalN

Proof of Theorem cmtvalN
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cmtfval.b . . . . . 6
2 cmtfval.j . . . . . 6
3 cmtfval.m . . . . . 6
4 cmtfval.o . . . . . 6
5 cmtfval.c . . . . . 6
61, 2, 3, 4, 5cmtfvalN 29847 . . . . 5
7 df-3an 938 . . . . . 6
87opabbii 4264 . . . . 5
96, 8syl6eq 2483 . . . 4
109breqd 4215 . . 3
12 df-br 4205 . . . 4
13 id 20 . . . . . 6
14 oveq1 6079 . . . . . . 7
15 oveq1 6079 . . . . . . 7
1614, 15oveq12d 6090 . . . . . 6
1713, 16eqeq12d 2449 . . . . 5
18 oveq2 6080 . . . . . . 7
19 fveq2 5719 . . . . . . . 8
2019oveq2d 6088 . . . . . . 7
2118, 20oveq12d 6090 . . . . . 6
2221eqeq2d 2446 . . . . 5
2317, 22opelopab2 4467 . . . 4
2412, 23syl5bb 249 . . 3