Theorem issetssr

Description: Two ways of expressing set existence. (Contributed by Peter Mazsa, 1-Aug-2019)

	Ref	Expression
Assertion	issetssr	$$⊢A\in \mathrm{V}\leftrightarrow A\mathrm{S}A$$

Proof

Step	Hyp	Ref	Expression
1		brssrid	$$⊢A\in \mathrm{V}\to A\mathrm{S}A$$
2		relssr	$$⊢\mathrm{Rel}\mathrm{S}$$
3	2	brrelex1i	$$⊢A\mathrm{S}A\to A\in \mathrm{V}$$
4	1 3	impbii	$$⊢A\in \mathrm{V}\leftrightarrow A\mathrm{S}A$$