Metamath Proof Explorer

Theorem structfun

Description: Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015) (Proof shortened by AV, 12-Nov-2021)

Ref Expression
Hypothesis structfun.1 
|- F Struct X
Assertion structfun 
|- Fun `' `' F

Proof

Step Hyp Ref Expression
1 structfun.1 
 |-  F Struct X
2 structfung 
 |-  ( F Struct X -> Fun `' `' F )
3 1 2 ax-mp 
 |-  Fun `' `' F