llyeq

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

		Ref	Expression
	Assertion	llyeq	$⊢ A = B \to LocallyA=LocallyB$

Step	Hyp	Ref	Expression
1		eleq2	$⊢ A = B \to (j ↾_{𝑡} u \in A \leftrightarrow j ↾_{𝑡} u \in B)$
2	1	anbi2d	$⊢ A = B \to ((y \in u \land j ↾_{𝑡} u \in A) \leftrightarrow (y \in u \land j ↾_{𝑡} u \in B))$
3	2	rexbidv	$⊢ A = B \to (\exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A) \leftrightarrow \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in B))$
4	3	2ralbidv	$⊢ A = B \to (\forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A) \leftrightarrow \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in B))$
5	4	rabbidv	$⊢ A = B \to \{j \in Top \| \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A)\} = \{j \in Top \| \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in B)\}$
6		df-lly	$⊢ LocallyA=\{j \in Top \| \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in A)\}$
7		df-lly	$⊢ LocallyB=\{j \in Top \| \forall x \in j \forall y \in x \exists u \in (j \cap 𝒫 x) (y \in u \land j ↾_{𝑡} u \in B)\}$
8	5 6 7	3eqtr4g	$⊢ A = B \to LocallyA=LocallyB$

Metamath Proof Explorer