Metamath Proof Explorer

Theorem acneq

Description: Equality theorem for the choice set function. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acneq 
|- ( A = C -> AC_ A = AC_ C )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( A = C -> ( A e. _V <-> C e. _V ) )
2 oveq2 
 |-  ( A = C -> ( ( ~P x \ { (/) } ) ^m A ) = ( ( ~P x \ { (/) } ) ^m C ) )
3 raleq 
 |-  ( A = C -> ( A. y e. A ( g ` y ) e. ( f ` y ) <-> A. y e. C ( g ` y ) e. ( f ` y ) ) )
4 3 exbidv 
 |-  ( A = C -> ( E. g A. y e. A ( g ` y ) e. ( f ` y ) <-> E. g A. y e. C ( g ` y ) e. ( f ` y ) ) )
5 2 4 raleqbidv 
 |-  ( A = C -> ( A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) <-> A. f e. ( ( ~P x \ { (/) } ) ^m C ) E. g A. y e. C ( g ` y ) e. ( f ` y ) ) )
6 1 5 anbi12d 
 |-  ( A = C -> ( ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) <-> ( C e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m C ) E. g A. y e. C ( g ` y ) e. ( f ` y ) ) ) )
7 6 abbidv 
 |-  ( A = C -> { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) } = { x | ( C e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m C ) E. g A. y e. C ( g ` y ) e. ( f ` y ) ) } )
8 df-acn 
 |-  AC_ A = { x | ( A e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m A ) E. g A. y e. A ( g ` y ) e. ( f ` y ) ) }
9 df-acn 
 |-  AC_ C = { x | ( C e. _V /\ A. f e. ( ( ~P x \ { (/) } ) ^m C ) E. g A. y e. C ( g ` y ) e. ( f ` y ) ) }
10 7 8 9 3eqtr4g 
 |-  ( A = C -> AC_ A = AC_ C )