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

Metamath Proof Explorer

Theorem elirrvOLD

Description: Obsolete version of elirrv as of 27-Dec-2025. (Contributed by NM, 19-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion elirrvOLD 
|- -. x e. x

Proof

Step Hyp Ref Expression
1 vsnex 
 |-  { x } e. _V
2 eleq1w 
 |-  ( y = x -> ( y e. { x } <-> x e. { x } ) )
3 vsnid 
 |-  x e. { x }
4 2 3 speivw 
 |-  E. y y e. { x }
5 zfregcl 
 |-  ( { x } e. _V -> ( E. y y e. { x } -> E. y e. { x } A. z e. y -. z e. { x } ) )
6 1 4 5 mp2 
 |-  E. y e. { x } A. z e. y -. z e. { x }
7 velsn 
 |-  ( y e. { x } <-> y = x )
8 ax9 
 |-  ( x = y -> ( x e. x -> x e. y ) )
9 8 equcoms 
 |-  ( y = x -> ( x e. x -> x e. y ) )
10 9 com12 
 |-  ( x e. x -> ( y = x -> x e. y ) )
11 7 10 biimtrid 
 |-  ( x e. x -> ( y e. { x } -> x e. y ) )
12 eleq1w 
 |-  ( z = x -> ( z e. { x } <-> x e. { x } ) )
13 12 notbid 
 |-  ( z = x -> ( -. z e. { x } <-> -. x e. { x } ) )
14 13 rspccv 
 |-  ( A. z e. y -. z e. { x } -> ( x e. y -> -. x e. { x } ) )
15 3 14 mt2i 
 |-  ( A. z e. y -. z e. { x } -> -. x e. y )
16 11 15 nsyli 
 |-  ( x e. x -> ( A. z e. y -. z e. { x } -> -. y e. { x } ) )
17 16 con2d 
 |-  ( x e. x -> ( y e. { x } -> -. A. z e. y -. z e. { x } ) )
18 17 ralrimiv 
 |-  ( x e. x -> A. y e. { x } -. A. z e. y -. z e. { x } )
19 ralnex 
 |-  ( A. y e. { x } -. A. z e. y -. z e. { x } <-> -. E. y e. { x } A. z e. y -. z e. { x } )
20 18 19 sylib 
 |-  ( x e. x -> -. E. y e. { x } A. z e. y -. z e. { x } )
21 6 20 mt2 
 |-  -. x e. x