Metamath Proof Explorer

Theorem hfadj

Description: Adjoining one HF element to an HF set preserves HF status. (Contributed by Scott Fenton, 15-Jul-2015)

Ref Expression
Assertion hfadj 
|- ( ( A e. Hf /\ B e. Hf ) -> ( A u. { B } ) e. Hf )

Proof

Step Hyp Ref Expression
1 hfsn 
 |-  ( B e. Hf -> { B } e. Hf )
2 hfun 
 |-  ( ( A e. Hf /\ { B } e. Hf ) -> ( A u. { B } ) e. Hf )
3 1 2 sylan2 
 |-  ( ( A e. Hf /\ B e. Hf ) -> ( A u. { B } ) e. Hf )