Theorem uvtx0

Description: There is no universal vertex if there is no vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 30-Oct-2020) (Proof shortened by AV, 14-Feb-2022)

	Ref	Expression
Hypothesis	uvtxel.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	uvtx0	$$⊢V=\varnothing \to \mathrm{UnivVtx}\left(G\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		uvtxel.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	uvtxval	$$⊢\mathrm{UnivVtx}\left(G\right)=\left\{v\in V|\forall n\in \left(V\setminus \left\{v\right\}\right)n\in \left(G\mathrm{NeighbVtx}v\right)\right\}$$
3		rabeq	$$⊢V=\varnothing \to \left\{v\in V|\forall n\in \left(V\setminus \left\{v\right\}\right)n\in \left(G\mathrm{NeighbVtx}v\right)\right\}=\left\{v\in \varnothing |\forall n\in \left(V\setminus \left\{v\right\}\right)n\in \left(G\mathrm{NeighbVtx}v\right)\right\}$$
4		rab0	$$⊢\left\{v\in \varnothing |\forall n\in \left(V\setminus \left\{v\right\}\right)n\in \left(G\mathrm{NeighbVtx}v\right)\right\}=\varnothing$$
5	3 4	eqtrdi	$$⊢V=\varnothing \to \left\{v\in V|\forall n\in \left(V\setminus \left\{v\right\}\right)n\in \left(G\mathrm{NeighbVtx}v\right)\right\}=\varnothing$$
6	2 5	eqtrid	$$⊢V=\varnothing \to \mathrm{UnivVtx}\left(G\right)=\varnothing$$