Step |
Hyp |
Ref |
Expression |
1 |
|
vex |
|- y e. _V |
2 |
1
|
elintrab |
|- ( y e. |^| { x e. B | A C_ x } <-> A. x e. B ( A C_ x -> y e. x ) ) |
3 |
|
ssid |
|- A C_ A |
4 |
|
sseq2 |
|- ( x = A -> ( A C_ x <-> A C_ A ) ) |
5 |
|
eleq2 |
|- ( x = A -> ( y e. x <-> y e. A ) ) |
6 |
4 5
|
imbi12d |
|- ( x = A -> ( ( A C_ x -> y e. x ) <-> ( A C_ A -> y e. A ) ) ) |
7 |
6
|
rspcv |
|- ( A e. B -> ( A. x e. B ( A C_ x -> y e. x ) -> ( A C_ A -> y e. A ) ) ) |
8 |
3 7
|
mpii |
|- ( A e. B -> ( A. x e. B ( A C_ x -> y e. x ) -> y e. A ) ) |
9 |
2 8
|
syl5bi |
|- ( A e. B -> ( y e. |^| { x e. B | A C_ x } -> y e. A ) ) |
10 |
9
|
ssrdv |
|- ( A e. B -> |^| { x e. B | A C_ x } C_ A ) |
11 |
|
ssintub |
|- A C_ |^| { x e. B | A C_ x } |
12 |
11
|
a1i |
|- ( A e. B -> A C_ |^| { x e. B | A C_ x } ) |
13 |
10 12
|
eqssd |
|- ( A e. B -> |^| { x e. B | A C_ x } = A ) |