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 ) } ) |
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 ) } ) |