Theorem hfadj

Description: Adjoining one hereditarily finite set to a hereditarily finite set results in a hereditarily finite set. (Contributed by Scott Fenton, 15-Jul-2015)

	Ref	Expression
Assertion	hfadj	Could not format assertion : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( A u. { B } ) e. HF ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		hfsn	Could not format ( B e. HF -> { B } e. HF ) : No typesetting found for |- ( B e. HF -> { B } e. HF ) with typecode |-
2		hfun	Could not format ( ( A e. HF /\ { B } e. HF ) -> ( A u. { B } ) e. HF ) : No typesetting found for |- ( ( A e. HF /\ { B } e. HF ) -> ( A u. { B } ) e. HF ) with typecode |-
3	1 2	sylan2	Could not format ( ( A e. HF /\ B e. HF ) -> ( A u. { B } ) e. HF ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> ( A u. { B } ) e. HF ) with typecode |-