Metamath Proof Explorer


Theorem brstruct

Description: The structure relation is a relation. (Contributed by Mario Carneiro, 29-Aug-2015)

Ref Expression
Assertion brstruct Rel Struct

Proof

Step Hyp Ref Expression
1 df-struct Struct = f x | x × Fun f dom f x
2 1 relopabiv Rel Struct