Theorem sclnbgrel

Description: Characterization of a member X of the semiclosed neighborhood of a vertex N in a graph G . (Contributed by AV, 16-May-2025)

	Ref	Expression
Hypotheses	dfsclnbgr2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	dfsclnbgr2.s	⊢ 𝑆 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 }
	dfsclnbgr2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	sclnbgrel	⊢ ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑋 } ⊆ 𝑒 ) )

Proof

Step	Hyp	Ref	Expression
1		dfsclnbgr2.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		dfsclnbgr2.s	⊢ 𝑆 = { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 }
3		dfsclnbgr2.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
4	2	eleq2i	⊢ ( 𝑋 ∈ 𝑆 ↔ 𝑋 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } )
5		preq2	⊢ ( 𝑛 = 𝑋 → { 𝑁 , 𝑛 } = { 𝑁 , 𝑋 } )
6	5	sseq1d	⊢ ( 𝑛 = 𝑋 → ( { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ { 𝑁 , 𝑋 } ⊆ 𝑒 ) )
7	6	rexbidv	⊢ ( 𝑛 = 𝑋 → ( ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 ↔ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑋 } ⊆ 𝑒 ) )
8	7	elrab	⊢ ( 𝑋 ∈ { 𝑛 ∈ 𝑉 ∣ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑛 } ⊆ 𝑒 } ↔ ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑋 } ⊆ 𝑒 ) )
9	4 8	bitri	⊢ ( 𝑋 ∈ 𝑆 ↔ ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑒 ∈ 𝐸 { 𝑁 , 𝑋 } ⊆ 𝑒 ) )