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

Metamath Proof Explorer

Theorem vex

Description: All setvar variables are sets (see isset ). Theorem 6.8 of Quine p. 43. A shorter proof is possible from eleq2i but it uses more axioms. (Contributed by NM, 26-May-1993) Remove use of ax-12 . (Revised by SN, 28-Aug-2023) (Proof shortened by BJ, 4-Sep-2024)

Ref Expression
Assertion vex 
|- x e. _V

Proof

Step Hyp Ref Expression
1 vextru 
 |-  x e. { x | T. }
2 dfv2 
 |-  _V = { x | T. }
3 1 2 eleqtrri 
 |-  x e. _V