NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-muc GIF 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 = (m NC , n NC {a b m g n a ≈ (b × g)})
Distinct variable group:   m,n,a,b,g

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