Theorem opnneibid2

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

	Ref	Expression
Hypotheses	opnneir.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
	opnneilv.2	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝜓 → 𝜒 ) )
	opnneil.3	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	opnneibid2	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		opnneir.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		opnneilv.2	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝜓 → 𝜒 ) )
3		opnneil.3	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) )
4	1 2 3	opnneibid	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 ↔ ∃ 𝑥 ∈ 𝐽 ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) ) )
5	3	opnneilem	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑆 ⊆ 𝑥 ∧ 𝜓 ) ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) )
6	4 5	bitrd	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 ↔ ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) )