This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )