Theorem issetri

Description: A way to say " A is a set" (inference form). (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Hypothesis	issetri.1	⊢ ∃ 𝑥 𝑥 = 𝐴
Assertion	issetri	⊢ 𝐴 ∈ V

Proof

Step	Hyp	Ref	Expression
1		issetri.1	⊢ ∃ 𝑥 𝑥 = 𝐴
2		isset	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑥 𝑥 = 𝐴 )
3	1 2	mpbir	⊢ 𝐴 ∈ V