Metamath Proof Explorer

Theorem nllyeq

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

Ref Expression
Assertion nllyeq ⊢ A = B → N-Locally A = N-Locally B

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ A = B → j ↾ 𝑡 u ∈ A ↔ j ↾ 𝑡 u ∈ B
2 1 rexbidv ⊢ A = B → ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A ↔ ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ B
3 2 2ralbidv ⊢ A = B → ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A ↔ ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ B
4 3 rabbidv ⊢ A = B → j ∈ Top | ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A = j ∈ Top | ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ B
5 df-nlly ⊢ N-Locally A = j ∈ Top | ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ A
6 df-nlly ⊢ N-Locally B = j ∈ Top | ∀ x ∈ j ∀ y ∈ x ∃ u ∈ nei ⁡ j ⁡ y ∩ 𝒫 x j ↾ 𝑡 u ∈ B
7 4 5 6 3eqtr4g ⊢ A = B → N-Locally A = N-Locally B