Theorem structex

Description: A structure is a set. (Contributed by AV, 10-Nov-2021)

	Ref	Expression
Assertion	structex	$$⊢G\mathrm{Struct}X\to G\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		brstruct	$$⊢\mathrm{Rel}\mathrm{Struct}$$
2	1	brrelex1i	$$⊢G\mathrm{Struct}X\to G\in \mathrm{V}$$