Metamath Proof Explorer

Theorem prfi

Description: An unordered pair is finite. (Contributed by NM, 22-Aug-2008)

Ref Expression
Assertion prfi 
|- { A , B } e. Fin

Proof

Step Hyp Ref Expression
1 df-pr 
 |-  { A , B } = ( { A } u. { B } )
2 snfi 
 |-  { A } e. Fin
3 snfi 
 |-  { B } e. Fin
4 unfi 
 |-  ( ( { A } e. Fin /\ { B } e. Fin ) -> ( { A } u. { B } ) e. Fin )
5 2 3 4 mp2an 
 |-  ( { A } u. { B } ) e. Fin
6 1 5 eqeltri 
 |-  { A , B } e. Fin