Description: The FOL statement used in the standard proof of Russell's paradox ru . (Contributed by NM, 7-Aug-1994) Extract from proof of ru and reduce axiom usage. (Revised by BJ, 12-Oct-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | ru0 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.19 | ||
2 | elequ1 | ||
3 | elequ12 | ||
4 | 3 | anidms | |
5 | 4 | notbid | |
6 | 2 5 | bibi12d | |
7 | 6 | spvv | |
8 | 1 7 | mto |