Theorem structex

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

	Ref	Expression
Assertion	structex	⊢ ( 𝐺 Struct 𝑋 → 𝐺 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		brstruct	⊢ Rel Struct
2	1	brrelex1i	⊢ ( 𝐺 Struct 𝑋 → 𝐺 ∈ V )