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 V
Assertion isseti x x = A

Proof

Step Hyp Ref Expression
1 isseti.1 A V
2 elissetv A V x x = A
3 1 2 ax-mp x x = A