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

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
2		hfsn	⊢ ( 𝐴 ∈ HF → { 𝐴 } ∈ HF )
3		hfadj	⊢ ( ( { 𝐴 } ∈ HF ∧ 𝐵 ∈ HF ) → ( { 𝐴 } ∪ { 𝐵 } ) ∈ HF )
4	2 3	sylan	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → ( { 𝐴 } ∪ { 𝐵 } ) ∈ HF )
5	1 4	eqeltrid	⊢ ( ( 𝐴 ∈ HF ∧ 𝐵 ∈ HF ) → { 𝐴 , 𝐵 } ∈ HF )