| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ral0 |
|- A. x e. (/) ( ~P x C_ (/) /\ ~P x e. (/) ) |
| 2 |
|
elsni |
|- ( x e. { (/) } -> x = (/) ) |
| 3 |
|
0ex |
|- (/) e. _V |
| 4 |
3
|
enref |
|- (/) ~~ (/) |
| 5 |
|
breq1 |
|- ( x = (/) -> ( x ~~ (/) <-> (/) ~~ (/) ) ) |
| 6 |
4 5
|
mpbiri |
|- ( x = (/) -> x ~~ (/) ) |
| 7 |
6
|
orcd |
|- ( x = (/) -> ( x ~~ (/) \/ x e. (/) ) ) |
| 8 |
2 7
|
syl |
|- ( x e. { (/) } -> ( x ~~ (/) \/ x e. (/) ) ) |
| 9 |
|
pw0 |
|- ~P (/) = { (/) } |
| 10 |
8 9
|
eleq2s |
|- ( x e. ~P (/) -> ( x ~~ (/) \/ x e. (/) ) ) |
| 11 |
10
|
rgen |
|- A. x e. ~P (/) ( x ~~ (/) \/ x e. (/) ) |
| 12 |
|
eltsk2g |
|- ( (/) e. _V -> ( (/) e. Tarski <-> ( A. x e. (/) ( ~P x C_ (/) /\ ~P x e. (/) ) /\ A. x e. ~P (/) ( x ~~ (/) \/ x e. (/) ) ) ) ) |
| 13 |
3 12
|
ax-mp |
|- ( (/) e. Tarski <-> ( A. x e. (/) ( ~P x C_ (/) /\ ~P x e. (/) ) /\ A. x e. ~P (/) ( x ~~ (/) \/ x e. (/) ) ) ) |
| 14 |
1 11 13
|
mpbir2an |
|- (/) e. Tarski |