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

Definition df-wun 9101
Description: The class of all weak universes. A weak universe is a nonempty transitive class closed under union, pairing, and powerset. The advantage of a weak universe over a Grothendieck universe is that weak universes satisfy the analogue uniwun 9139 of grothtsk 9234 in ZFC (whereas grothtsk 9234 requires ax-groth 9222). (Contributed by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
df-wun
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-wun
StepHypRef Expression
1 cwun 9099 . 2
2 vu . . . . . 6
32cv 1394 . . . . 5
43wtr 4545 . . . 4
5 c0 3784 . . . . 5
63, 5wne 2652 . . . 4
7 vx . . . . . . . . 9
87cv 1394 . . . . . . . 8
98cuni 4249 . . . . . . 7
109, 3wcel 1818 . . . . . 6
118cpw 4012 . . . . . . 7
1211, 3wcel 1818 . . . . . 6
13 vy . . . . . . . . . 10
1413cv 1394 . . . . . . . . 9
158, 14cpr 4031 . . . . . . . 8
1615, 3wcel 1818 . . . . . . 7
1716, 13, 3wral 2807 . . . . . 6
1810, 12, 17w3a 973 . . . . 5
1918, 7, 3wral 2807 . . . 4
204, 6, 19w3a 973 . . 3
2120, 2cab 2442 . 2
221, 21wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  iswun  9103
  Copyright terms: Public domain W3C validator