Metamath Proof Explorer


Theorem opnneir

Description: If something is true for an open neighborhood, it must be true for a neighborhood. (Contributed by Zhi Wang, 31-Aug-2024)

Ref Expression
Hypothesis opnneir.1 φJTop
Assertion opnneir φxJSxψxneiJSψ

Proof

Step Hyp Ref Expression
1 opnneir.1 φJTop
2 anass xJSxψxJSxψ
3 opnneiss JTopxJSxxneiJS
4 3 3expib JTopxJSxxneiJS
5 4 anim1d JTopxJSxψxneiJSψ
6 2 5 biimtrrid JTopxJSxψxneiJSψ
7 6 reximdv2 JTopxJSxψxneiJSψ
8 1 7 syl φxJSxψxneiJSψ