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 𝐴 ∈ V
Assertion isseti 𝑥 𝑥 = 𝐴

Proof

Step Hyp Ref Expression
1 isseti.1 𝐴 ∈ V
2 elissetv ( 𝐴 ∈ V → ∃ 𝑥 𝑥 = 𝐴 )
3 1 2 ax-mp 𝑥 𝑥 = 𝐴