Theorem structn0fun

Description: A structure without the empty set is a function. (Contributed by AV, 13-Nov-2021)

	Ref	Expression
Assertion	structn0fun	⊢ ( 𝐹 Struct 𝑋 → Fun ( 𝐹 ∖ { ∅ } ) )

Proof

Step	Hyp	Ref	Expression
1		isstruct2	⊢ ( 𝐹 Struct 𝑋 ↔ ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) )
2	1	simp2bi	⊢ ( 𝐹 Struct 𝑋 → Fun ( 𝐹 ∖ { ∅ } ) )