Theorem hfpr

Description: A pair whose members are hereditarily finite sets is a hereditarily finite set. (Contributed by Eric Schmidt, 26-Sep-2026)

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

Proof

Step	Hyp	Ref	Expression
1		df-pr	$$⊢\left\{A,B\right\}=\left\{A\right\}\cup \left\{B\right\}$$
2		hfsn	Could not format ( A e. HF -> { A } e. HF ) : No typesetting found for |- ( A e. HF -> { A } e. HF ) with typecode |-
3		hfadj	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 |-
4	2 3	sylan	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 |-
5	1 4	eqeltrid	Could not format ( ( A e. HF /\ B e. HF ) -> { A , B } e. HF ) : No typesetting found for |- ( ( A e. HF /\ B e. HF ) -> { A , B } e. HF ) with typecode |-