This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ruOLD

Description: Obsolete version of ru as of 20-Jun-2025. (Contributed by NM, 7-Aug-1994) Remove use of ax-13 . (Revised by BJ, 12-Oct-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ruOLD 
|- { x | x e/ x } e/ _V

Proof

Step Hyp Ref Expression
1 pm5.19 
 |-  -. ( y e. y <-> -. y e. y )
2 eleq1w 
 |-  ( x = y -> ( x e. y <-> y e. y ) )
3 df-nel 
 |-  ( x e/ x <-> -. x e. x )
4 id 
 |-  ( x = y -> x = y )
5 4 4 eleq12d 
 |-  ( x = y -> ( x e. x <-> y e. y ) )
6 5 notbid 
 |-  ( x = y -> ( -. x e. x <-> -. y e. y ) )
7 3 6 bitrid 
 |-  ( x = y -> ( x e/ x <-> -. y e. y ) )
8 2 7 bibi12d 
 |-  ( x = y -> ( ( x e. y <-> x e/ x ) <-> ( y e. y <-> -. y e. y ) ) )
9 8 spvv 
 |-  ( A. x ( x e. y <-> x e/ x ) -> ( y e. y <-> -. y e. y ) )
10 1 9 mto 
 |-  -. A. x ( x e. y <-> x e/ x )
11 eqabb 
 |-  ( y = { x | x e/ x } <-> A. x ( x e. y <-> x e/ x ) )
12 10 11 mtbir 
 |-  -. y = { x | x e/ x }
13 12 nex 
 |-  -. E. y y = { x | x e/ x }
14 isset 
 |-  ( { x | x e/ x } e. _V <-> E. y y = { x | x e/ x } )
15 13 14 mtbir 
 |-  -. { x | x e/ x } e. _V
16 15 nelir 
 |-  { x | x e/ x } e/ _V