Metamath Proof Explorer
Description: The FOL part of Russell's paradox ru (see also bj-ru1 , bj-ru ).
Use of elequ1 , bj-elequ12 (instead of eleq1 , eleq12d as in
ru ) permits to remove dependency on ax-10 , ax-11 , ax-12 ,
ax-ext , df-sb , df-clab , df-cleq , df-clel . (Contributed by BJ, 12-Oct-2019) (Proof modification is discouraged.)
|
|
Ref |
Expression |
|
Assertion |
bj-ru0 |
|- -. A. x ( x e. y <-> -. x e. x ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
pm5.19 |
|- -. ( y e. y <-> -. y e. y ) |
| 2 |
|
elequ1 |
|- ( x = y -> ( x e. y <-> y e. y ) ) |
| 3 |
|
bj-elequ12 |
|- ( ( x = y /\ x = y ) -> ( x e. x <-> y e. y ) ) |
| 4 |
3
|
anidms |
|- ( x = y -> ( x e. x <-> y e. y ) ) |
| 5 |
4
|
notbid |
|- ( x = y -> ( -. x e. x <-> -. y e. y ) ) |
| 6 |
2 5
|
bibi12d |
|- ( x = y -> ( ( x e. y <-> -. x e. x ) <-> ( y e. y <-> -. y e. y ) ) ) |
| 7 |
6
|
spvv |
|- ( A. x ( x e. y <-> -. x e. x ) -> ( y e. y <-> -. y e. y ) ) |
| 8 |
1 7
|
mto |
|- -. A. x ( x e. y <-> -. x e. x ) |