Step |
Hyp |
Ref |
Expression |
1 |
|
intid.1 |
|- A e. _V |
2 |
|
snex |
|- { A } e. _V |
3 |
|
eleq2 |
|- ( x = { A } -> ( A e. x <-> A e. { A } ) ) |
4 |
1
|
snid |
|- A e. { A } |
5 |
3 4
|
intmin3 |
|- ( { A } e. _V -> |^| { x | A e. x } C_ { A } ) |
6 |
2 5
|
ax-mp |
|- |^| { x | A e. x } C_ { A } |
7 |
1
|
elintab |
|- ( A e. |^| { x | A e. x } <-> A. x ( A e. x -> A e. x ) ) |
8 |
|
id |
|- ( A e. x -> A e. x ) |
9 |
7 8
|
mpgbir |
|- A e. |^| { x | A e. x } |
10 |
|
snssi |
|- ( A e. |^| { x | A e. x } -> { A } C_ |^| { x | A e. x } ) |
11 |
9 10
|
ax-mp |
|- { A } C_ |^| { x | A e. x } |
12 |
6 11
|
eqssi |
|- |^| { x | A e. x } = { A } |