Theorem uvtxusgr

Description: The set of all universal vertices of a simple graph. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 31-Oct-2020)

	Ref	Expression
Hypotheses	uvtxnbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	uvtxusgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	uvtxusgr	⊢ ( 𝐺 ∈ USGraph → ( UnivVtx ‘ 𝐺 ) = { 𝑛 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) { 𝑘 , 𝑛 } ∈ 𝐸 } )

Proof

Step	Hyp	Ref	Expression
1		uvtxnbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		uvtxusgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1	uvtxval	⊢ ( UnivVtx ‘ 𝐺 ) = { 𝑛 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) 𝑘 ∈ ( 𝐺 NeighbVtx 𝑛 ) }
4	2	nbusgreledg	⊢ ( 𝐺 ∈ USGraph → ( 𝑘 ∈ ( 𝐺 NeighbVtx 𝑛 ) ↔ { 𝑘 , 𝑛 } ∈ 𝐸 ) )
5	4	ralbidv	⊢ ( 𝐺 ∈ USGraph → ( ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) 𝑘 ∈ ( 𝐺 NeighbVtx 𝑛 ) ↔ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) { 𝑘 , 𝑛 } ∈ 𝐸 ) )
6	5	rabbidv	⊢ ( 𝐺 ∈ USGraph → { 𝑛 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) 𝑘 ∈ ( 𝐺 NeighbVtx 𝑛 ) } = { 𝑛 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) { 𝑘 , 𝑛 } ∈ 𝐸 } )
7	3 6	syl5eq	⊢ ( 𝐺 ∈ USGraph → ( UnivVtx ‘ 𝐺 ) = { 𝑛 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) { 𝑘 , 𝑛 } ∈ 𝐸 } )