NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-muc Unicode version

Definition df-muc 6102
Description: Define cardinal multiplication. Definition from [Rosser] p. 378. (Contributed by Scott Fenton, 24-Feb-2015.)
Assertion
Ref Expression
df-muc ·c NC NC
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-muc
StepHypRef Expression
1 cmuc 6092 . 2 ·c
2 vm . . 3
3 vn . . 3
4 cncs 6088 . . 3 NC
5 va . . . . . . . 8
65cv 1641 . . . . . . 7
7 vb . . . . . . . . 9
87cv 1641 . . . . . . . 8
9 vg . . . . . . . . 9
109cv 1641 . . . . . . . 8
118, 10cxp 4770 . . . . . . 7
12 cen 6028 . . . . . . 7
136, 11, 12wbr 4639 . . . . . 6
143cv 1641 . . . . . 6
1513, 9, 14wrex 2615 . . . . 5
162cv 1641 . . . . 5
1715, 7, 16wrex 2615 . . . 4
1817, 5cab 2339 . . 3
192, 3, 4, 4, 18cmpt2 5653 . 2 NC NC
201, 19wceq 1642 1 ·c NC NC
Colors of variables: wff setvar class
This definition is referenced by:  ovmuc  6130  mucex  6133
  Copyright terms: Public domain W3C validator