Theorem llyeq

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

	Ref	Expression
Assertion	llyeq	⊢ ( 𝐴 = 𝐵 → Locally 𝐴 = Locally 𝐵 )

Proof

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