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

Definition df-irred 15750
 Description: Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
Assertion
Ref Expression
df-irred Irred Unit
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-irred
StepHypRef Expression
1 cir 15747 . 2 Irred
2 vw . . 3
3 cvv 2958 . . 3
4 vb . . . 4
52cv 1652 . . . . . 6
6 cbs 13471 . . . . . 6
75, 6cfv 5456 . . . . 5
8 cui 15746 . . . . . 6 Unit
95, 8cfv 5456 . . . . 5 Unit
107, 9cdif 3319 . . . 4 Unit
11 vx . . . . . . . . . 10
1211cv 1652 . . . . . . . . 9
13 vy . . . . . . . . . 10
1413cv 1652 . . . . . . . . 9
15 cmulr 13532 . . . . . . . . . 10
165, 15cfv 5456 . . . . . . . . 9
1712, 14, 16co 6083 . . . . . . . 8
18 vz . . . . . . . . 9
1918cv 1652 . . . . . . . 8
2017, 19wne 2601 . . . . . . 7
214cv 1652 . . . . . . 7
2220, 13, 21wral 2707 . . . . . 6
2322, 11, 21wral 2707 . . . . 5
2423, 18, 21crab 2711 . . . 4
254, 10, 24csb 3253 . . 3 Unit
262, 3, 25cmpt 4268 . 2 Unit
271, 26wceq 1653 1 Irred Unit
 Colors of variables: wff set class This definition is referenced by:  isirred  15806
 Copyright terms: Public domain W3C validator