Step |
Hyp |
Ref |
Expression |
1 |
|
rabssf.1 |
|- F/_ x B |
2 |
|
df-rab |
|- { x e. A | ph } = { x | ( x e. A /\ ph ) } |
3 |
2
|
sseq1i |
|- ( { x e. A | ph } C_ B <-> { x | ( x e. A /\ ph ) } C_ B ) |
4 |
1
|
abssf |
|- ( { x | ( x e. A /\ ph ) } C_ B <-> A. x ( ( x e. A /\ ph ) -> x e. B ) ) |
5 |
|
impexp |
|- ( ( ( x e. A /\ ph ) -> x e. B ) <-> ( x e. A -> ( ph -> x e. B ) ) ) |
6 |
5
|
albii |
|- ( A. x ( ( x e. A /\ ph ) -> x e. B ) <-> A. x ( x e. A -> ( ph -> x e. B ) ) ) |
7 |
|
df-ral |
|- ( A. x e. A ( ph -> x e. B ) <-> A. x ( x e. A -> ( ph -> x e. B ) ) ) |
8 |
6 7
|
bitr4i |
|- ( A. x ( ( x e. A /\ ph ) -> x e. B ) <-> A. x e. A ( ph -> x e. B ) ) |
9 |
3 4 8
|
3bitri |
|- ( { x e. A | ph } C_ B <-> A. x e. A ( ph -> x e. B ) ) |