Metamath Proof Explorer

Theorem bj-ru1

Description: A version of Russell's paradox ru (see also bj-ru ). (Contributed by BJ, 12-Oct-2019) (Proof modification is discouraged.)

Ref Expression
Assertion bj-ru1 
|- -. E. y y = { x | -. x e. x }

Proof

Step Hyp Ref Expression
1 bj-ru0 
 |-  -. A. x ( x e. y <-> -. x e. x )
2 abeq2 
 |-  ( y = { x | -. x e. x } <-> A. x ( x e. y <-> -. x e. x ) )
3 1 2 mtbir 
 |-  -. y = { x | -. x e. x }
4 3 nex 
 |-  -. E. y y = { x | -. x e. x }