Metamath Proof Explorer


Theorem opnneieqvv

Description: The equivalence between neighborhood and open neighborhood. A variant of opnneieqv with two dummy variables. (Contributed by Zhi Wang, 31-Aug-2024)

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

Proof

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