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	⊢ ( ( 𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → ( 𝐴 ∪ { 𝐵 } ) ∈ Hf )

Proof

Step	Hyp	Ref	Expression
1		hfsn	⊢ ( 𝐵 ∈ Hf → { 𝐵 } ∈ Hf )
2		hfun	⊢ ( ( 𝐴 ∈ Hf ∧ { 𝐵 } ∈ Hf ) → ( 𝐴 ∪ { 𝐵 } ) ∈ Hf )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ Hf ∧ 𝐵 ∈ Hf ) → ( 𝐴 ∪ { 𝐵 } ) ∈ Hf )