Description: Remove dependency on ax-13 (and df-v ) from Russell's paradox ru expressed with primitive symbols and with a class variable V . Note the more economical use of elissetv instead of isset to avoid use of df-v . (Contributed by BJ, 12-Oct-2019) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-ru | |- -. { x | -. x e. x } e. V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bj-ru1 | |- -. E. y y = { x | -. x e. x } |
|
| 2 | elissetv | |- ( { x | -. x e. x } e. V -> E. y y = { x | -. x e. x } ) |
|
| 3 | 1 2 | mto | |- -. { x | -. x e. x } e. V |