Theorem structex

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

	Ref	Expression
Assertion	structex	|- ( G Struct X -> G e. _V )

Proof

Step	Hyp	Ref	Expression
1		brstruct	|- Rel Struct
2	1	brrelex1i	|- ( G Struct X -> G e. _V )