Theorem llyeq

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

	Ref	Expression
Assertion	llyeq	|- ( A = B -> Locally A = Locally B )

Proof

Step	Hyp	Ref	Expression
1		eleq2	|- ( A = B -> ( ( j |`t u ) e. A <-> ( j |`t u ) e. B ) )
2	1	anbi2d	|- ( A = B -> ( ( y e. u /\ ( j |`t u ) e. A ) <-> ( y e. u /\ ( j |`t u ) e. B ) ) )
3	2	rexbidv	|- ( A = B -> ( E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) <-> E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. B ) ) )
4	3	2ralbidv	|- ( A = B -> ( A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) <-> A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. B ) ) )
5	4	rabbidv	|- ( A = B -> { j e. Top | A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) } = { j e. Top | A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. B ) } )
6		df-lly	|- Locally A = { j e. Top | A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. A ) }
7		df-lly	|- Locally B = { j e. Top | A. x e. j A. y e. x E. u e. ( j i^i ~P x ) ( y e. u /\ ( j |`t u ) e. B ) }
8	5 6 7	3eqtr4g	|- ( A = B -> Locally A = Locally B )