Step |
Hyp |
Ref |
Expression |
1 |
|
dfss2f.1 |
|- F/_ x A |
2 |
|
dfss2f.2 |
|- F/_ x B |
3 |
|
dfss2 |
|- ( A C_ B <-> A. z ( z e. A -> z e. B ) ) |
4 |
1
|
nfcri |
|- F/ x z e. A |
5 |
2
|
nfcri |
|- F/ x z e. B |
6 |
4 5
|
nfim |
|- F/ x ( z e. A -> z e. B ) |
7 |
|
nfv |
|- F/ z ( x e. A -> x e. B ) |
8 |
|
eleq1w |
|- ( z = x -> ( z e. A <-> x e. A ) ) |
9 |
|
eleq1w |
|- ( z = x -> ( z e. B <-> x e. B ) ) |
10 |
8 9
|
imbi12d |
|- ( z = x -> ( ( z e. A -> z e. B ) <-> ( x e. A -> x e. B ) ) ) |
11 |
6 7 10
|
cbvalv1 |
|- ( A. z ( z e. A -> z e. B ) <-> A. x ( x e. A -> x e. B ) ) |
12 |
3 11
|
bitri |
|- ( A C_ B <-> A. x ( x e. A -> x e. B ) ) |