Metamath Proof Explorer


Theorem opnneieqv

Description: The equivalence between neighborhood and open neighborhood. See opnneieqvv for different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024)

Ref Expression
Hypotheses opnneir.1 φJTop
opnneilv.2 φyxψχ
opnneil.3 φx=yψχ
Assertion opnneieqv φxneiJSψxJSxψ

Proof

Step Hyp Ref Expression
1 opnneir.1 φJTop
2 opnneilv.2 φyxψχ
3 opnneil.3 φx=yψχ
4 1 2 3 opnneil φxneiJSψxJSxψ
5 1 opnneir φxJSxψxneiJSψ
6 4 5 impbid φxneiJSψxJSxψ