Step |
Hyp |
Ref |
Expression |
1 |
|
idn2 |
|- (. A e. B ,. x = A ->. x = A ). |
2 |
|
3mix3 |
|- ( x = A -> ( x = C \/ x = D \/ x = A ) ) |
3 |
1 2
|
e2 |
|- (. A e. B ,. x = A ->. ( x = C \/ x = D \/ x = A ) ). |
4 |
|
abid |
|- ( x e. { x | ( x = C \/ x = D \/ x = A ) } <-> ( x = C \/ x = D \/ x = A ) ) |
5 |
3 4
|
e2bir |
|- (. A e. B ,. x = A ->. x e. { x | ( x = C \/ x = D \/ x = A ) } ). |
6 |
|
dftp2 |
|- { C , D , A } = { x | ( x = C \/ x = D \/ x = A ) } |
7 |
6
|
eleq2i |
|- ( x e. { C , D , A } <-> x e. { x | ( x = C \/ x = D \/ x = A ) } ) |
8 |
5 7
|
e2bir |
|- (. A e. B ,. x = A ->. x e. { C , D , A } ). |
9 |
|
eleq1 |
|- ( x = A -> ( x e. { C , D , A } <-> A e. { C , D , A } ) ) |
10 |
9
|
biimpd |
|- ( x = A -> ( x e. { C , D , A } -> A e. { C , D , A } ) ) |
11 |
1 8 10
|
e22 |
|- (. A e. B ,. x = A ->. A e. { C , D , A } ). |
12 |
11
|
in2 |
|- (. A e. B ->. ( x = A -> A e. { C , D , A } ) ). |
13 |
12
|
gen11 |
|- (. A e. B ->. A. x ( x = A -> A e. { C , D , A } ) ). |
14 |
|
19.23v |
|- ( A. x ( x = A -> A e. { C , D , A } ) <-> ( E. x x = A -> A e. { C , D , A } ) ) |
15 |
13 14
|
e1bi |
|- (. A e. B ->. ( E. x x = A -> A e. { C , D , A } ) ). |
16 |
|
idn1 |
|- (. A e. B ->. A e. B ). |
17 |
|
elisset |
|- ( A e. B -> E. x x = A ) |
18 |
16 17
|
e1a |
|- (. A e. B ->. E. x x = A ). |
19 |
|
id |
|- ( ( E. x x = A -> A e. { C , D , A } ) -> ( E. x x = A -> A e. { C , D , A } ) ) |
20 |
15 18 19
|
e11 |
|- (. A e. B ->. A e. { C , D , A } ). |
21 |
20
|
in1 |
|- ( A e. B -> A e. { C , D , A } ) |