Theorem nllyeq

Description: Equality theorem for the Locally A predicate. (Contributed by Mario Carneiro, 2-Mar-2015)

	Ref	Expression
Assertion	nllyeq	⊢ ( 𝐴 = 𝐵 → 𝑛-Locally 𝐴 = 𝑛-Locally 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eleq2	⊢ ( 𝐴 = 𝐵 → ( ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ↔ ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 ) )
2	1	rexbidv	⊢ ( 𝐴 = 𝐵 → ( ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ↔ ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 ) )
3	2	2ralbidv	⊢ ( 𝐴 = 𝐵 → ( ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 ↔ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 ) )
4	3	rabbidv	⊢ ( 𝐴 = 𝐵 → { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 } = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 } )
5		df-nlly	⊢ 𝑛-Locally 𝐴 = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐴 }
6		df-nlly	⊢ 𝑛-Locally 𝐵 = { 𝑗 ∈ Top ∣ ∀ 𝑥 ∈ 𝑗 ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ ( ( ( nei ‘ 𝑗 ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( 𝑗 ↾t 𝑢 ) ∈ 𝐵 }
7	4 5 6	3eqtr4g	⊢ ( 𝐴 = 𝐵 → 𝑛-Locally 𝐴 = 𝑛-Locally 𝐵 )