This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )