Metamath Proof Explorer

Theorem vexOLD

Description: Obsolete version of vex as of 4-Sep-2024. (Contributed by NM, 26-May-1993) Remove use of ax-12 . (Revised by SN, 28-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion vexOLD 
|- x e. _V

Proof

Step Hyp Ref Expression
1 equid 
 |-  x = x
2 1 vexw 
 |-  x e. { x | x = x }
3 df-v 
 |-  _V = { x | x = x }
4 2 3 eleqtrri 
 |-  x e. _V