Theorem clnbgrprc0

Description: The closed neighborhood is empty if the graph G or the vertex N are proper classes. (Contributed by AV, 7-May-2025)

	Ref	Expression
Assertion	clnbgrprc0	Could not format assertion : No typesetting found for |- ( -. ( G e. _V /\ N e. _V ) -> ( G ClNeighbVtx N ) = (/) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-clnbgr	Could not format ClNeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> ( { v } u. { n e. ( Vtx ` g ) | E. e e. ( Edg ` g ) { v , n } C_ e } ) ) : No typesetting found for |- ClNeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> ( { v } u. { n e. ( Vtx ` g ) | E. e e. ( Edg ` g ) { v , n } C_ e } ) ) with typecode |-
2	1	reldmmpo	Could not format Rel dom ClNeighbVtx : No typesetting found for |- Rel dom ClNeighbVtx with typecode |-
3	2	ovprc	Could not format ( -. ( G e. _V /\ N e. _V ) -> ( G ClNeighbVtx N ) = (/) ) : No typesetting found for |- ( -. ( G e. _V /\ N e. _V ) -> ( G ClNeighbVtx N ) = (/) ) with typecode |-