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