Step |
Hyp |
Ref |
Expression |
1 |
|
rabss3d.1 |
|- ( ( ph /\ ( x e. A /\ ps ) ) -> x e. B ) |
2 |
|
nfv |
|- F/ x ph |
3 |
|
nfrab1 |
|- F/_ x { x e. A | ps } |
4 |
|
nfrab1 |
|- F/_ x { x e. B | ps } |
5 |
|
simprr |
|- ( ( ph /\ ( x e. A /\ ps ) ) -> ps ) |
6 |
1 5
|
jca |
|- ( ( ph /\ ( x e. A /\ ps ) ) -> ( x e. B /\ ps ) ) |
7 |
6
|
ex |
|- ( ph -> ( ( x e. A /\ ps ) -> ( x e. B /\ ps ) ) ) |
8 |
|
rabid |
|- ( x e. { x e. A | ps } <-> ( x e. A /\ ps ) ) |
9 |
|
rabid |
|- ( x e. { x e. B | ps } <-> ( x e. B /\ ps ) ) |
10 |
7 8 9
|
3imtr4g |
|- ( ph -> ( x e. { x e. A | ps } -> x e. { x e. B | ps } ) ) |
11 |
2 3 4 10
|
ssrd |
|- ( ph -> { x e. A | ps } C_ { x e. B | ps } ) |