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 ( 𝐺 Struct 𝑋 → 𝐺 ∈ V )

Proof

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