Metamath Proof Explorer


Theorem isseti

Description: A way to say " A is a set" (inference form). (Contributed by NM, 24-Jun-1993) Remove dependencies on axioms. (Revised by BJ, 13-Jul-2019)

Ref Expression
Hypothesis isseti.1
|- A e. _V
Assertion isseti
|- E. x x = A

Proof

Step Hyp Ref Expression
1 isseti.1
 |-  A e. _V
2 elissetv
 |-  ( A e. _V -> E. x x = A )
3 1 2 ax-mp
 |-  E. x x = A