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 ∈ Hf ∧ B ∈ Hf → A ∪ B ∈ Hf

Proof

Step Hyp Ref Expression
1 hfsn ⊢ B ∈ Hf → B ∈ Hf
2 hfun ⊢ A ∈ Hf ∧ B ∈ Hf → A ∪ B ∈ Hf
3 1 2 sylan2 ⊢ A ∈ Hf ∧ B ∈ Hf → A ∪ B ∈ Hf