Theorem uniwun

Description: Every set is contained in a weak universe. This is the analogue of grothtsk for weak universes, but it is provable in ZF without the Tarski-Grothendieck axiom, contrary to grothtsk . (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	uniwun	|- U. WUni = _V

Proof

Step	Hyp	Ref	Expression
1		eqv	|- ( U. WUni = _V <-> A. x x e. U. WUni )
2		vsnex	|- { x } e. _V
3		wunex	|- ( { x } e. _V -> E. u e. WUni { x } C_ u )
4	2 3	ax-mp	|- E. u e. WUni { x } C_ u
5		eluni2	|- ( x e. U. WUni <-> E. u e. WUni x e. u )
6		vex	|- x e. _V
7	6	snss	|- ( x e. u <-> { x } C_ u )
8	7	rexbii	|- ( E. u e. WUni x e. u <-> E. u e. WUni { x } C_ u )
9	5 8	bitri	|- ( x e. U. WUni <-> E. u e. WUni { x } C_ u )
10	4 9	mpbir	|- x e. U. WUni
11	1 10	mpgbir	|- U. WUni = _V