Metamath Proof Explorer

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 
|- ( ( A e. HF /\ B e. HF ) -> { A , B } e. HF )

Proof

Step Hyp Ref Expression
1 df-pr 
 |-  { A , B } = ( { A } u. { B } )
2 hfsn 
 |-  ( A e. HF -> { A } e. HF )
3 hfadj 
 |-  ( ( { A } e. HF /\ B e. HF ) -> ( { A } u. { B } ) e. HF )
4 2 3 sylan 
 |-  ( ( A e. HF /\ B e. HF ) -> ( { A } u. { B } ) e. HF )
5 1 4 eqeltrid 
 |-  ( ( A e. HF /\ B e. HF ) -> { A , B } e. HF )