Metamath Proof Explorer
Description: A way to say " A is a set" (inference form). (Contributed by NM, 24Jun1993) Remove dependencies on axioms. (Revised by BJ, 13Jul2019)


Ref 
Expression 

Hypothesis 
isseti.1 
$${\u22a2}{A}\in \mathrm{V}$$ 

Assertion 
isseti 
$${\u22a2}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

isseti.1 
$${\u22a2}{A}\in \mathrm{V}$$ 
2 

elisset 
$${\u22a2}{A}\in \mathrm{V}\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$$ 
3 
1 2

axmp 
$${\u22a2}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={A}$$ 