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 bj-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 | bj-elissetv | |- ( { x | -. x e. x } e. V -> E. y y = { x | -. x e. x } ) |
|
3 | 1 2 | mto | |- -. { x | -. x e. x } e. V |