| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ssbr |
|- ( A C_ B -> ( y A z -> y B z ) ) |
| 2 |
1
|
anim2d |
|- ( A C_ B -> ( ( x C y /\ y A z ) -> ( x C y /\ y B z ) ) ) |
| 3 |
2
|
eximdv |
|- ( A C_ B -> ( E. y ( x C y /\ y A z ) -> E. y ( x C y /\ y B z ) ) ) |
| 4 |
3
|
ssopab2dv |
|- ( A C_ B -> { <. x , z >. | E. y ( x C y /\ y A z ) } C_ { <. x , z >. | E. y ( x C y /\ y B z ) } ) |
| 5 |
|
df-co |
|- ( A o. C ) = { <. x , z >. | E. y ( x C y /\ y A z ) } |
| 6 |
|
df-co |
|- ( B o. C ) = { <. x , z >. | E. y ( x C y /\ y B z ) } |
| 7 |
4 5 6
|
3sstr4g |
|- ( A C_ B -> ( A o. C ) C_ ( B o. C ) ) |