Metamath Proof Explorer


Theorem bj-cleq

Description: Substitution property for certain classes. (Contributed by BJ, 2-Apr-2019)

Ref Expression
Assertion bj-cleq
|- ( A = B -> { x | { x } e. ( A " C ) } = { x | { x } e. ( B " C ) } )

Proof

Step Hyp Ref Expression
1 imaeq1
 |-  ( A = B -> ( A " C ) = ( B " C ) )
2 eleq2
 |-  ( ( A " C ) = ( B " C ) -> ( { x } e. ( A " C ) <-> { x } e. ( B " C ) ) )
3 2 alrimiv
 |-  ( ( A " C ) = ( B " C ) -> A. x ( { x } e. ( A " C ) <-> { x } e. ( B " C ) ) )
4 abbi1
 |-  ( A. x ( { x } e. ( A " C ) <-> { x } e. ( B " C ) ) -> { x | { x } e. ( A " C ) } = { x | { x } e. ( B " C ) } )
5 1 3 4 3syl
 |-  ( A = B -> { x | { x } e. ( A " C ) } = { x | { x } e. ( B " C ) } )