Metamath Proof Explorer


Theorem opnneirv

Description: A variant of opnneir with different dummy variables. (Contributed by Zhi Wang, 31-Aug-2024)

Ref Expression
Hypotheses opnneir.1 ( 𝜑𝐽 ∈ Top )
opnneirv.2 ( ( 𝜑𝑥 = 𝑦 ) → ( 𝜓𝜒 ) )
Assertion opnneirv ( 𝜑 → ( ∃ 𝑥𝐽 ( 𝑆𝑥𝜓 ) → ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜒 ) )

Proof

Step Hyp Ref Expression
1 opnneir.1 ( 𝜑𝐽 ∈ Top )
2 opnneirv.2 ( ( 𝜑𝑥 = 𝑦 ) → ( 𝜓𝜒 ) )
3 2 opnneilem ( 𝜑 → ( ∃ 𝑥𝐽 ( 𝑆𝑥𝜓 ) ↔ ∃ 𝑦𝐽 ( 𝑆𝑦𝜒 ) ) )
4 1 opnneir ( 𝜑 → ( ∃ 𝑦𝐽 ( 𝑆𝑦𝜒 ) → ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜒 ) )
5 3 4 sylbid ( 𝜑 → ( ∃ 𝑥𝐽 ( 𝑆𝑥𝜓 ) → ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜒 ) )