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 ‘ 𝐺 ) = { 𝑛 ∈ 𝑉 ∣ ∀ 𝑘 ∈ ( 𝑉 ∖ { 𝑛 } ) { 𝑘 , 𝑛 } ∈ 𝐸 } ) |