Theorem prfi 9326

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

Assertion

Ref	Expression
prfi	⊢ {𝐴, 𝐵} ∈ Fin

Proof of Theorem prfi

Step	Hyp	Ref	Expression
1		df-pr 4632	. 2 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
2		snfi 9048	. . 3 ⊢ {𝐴} ∈ Fin
3		snfi 9048	. . 3 ⊢ {𝐵} ∈ Fin
4		unfi 9176	. . 3 ⊢ (({𝐴} ∈ Fin ∧ {𝐵} ∈ Fin) → ({𝐴} ∪ {𝐵}) ∈ Fin)
5	2, 3, 4	mp2an 688	. 2 ⊢ ({𝐴} ∪ {𝐵}) ∈ Fin
6	1, 5	eqeltri 2827	1 ⊢ {𝐴, 𝐵} ∈ Fin

Syntax hints:   ∈ wcel 2104   ∪ cun 3947  {csn 4629  {cpr 4631  Fincfn 8943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-om 7860  df-1o 8470  df-en 8944  df-fin 8947

This theorem is referenced by:  tpfi  9327  fiint  9328  inelfi  9417  tskpr  10769  hashpw  14402  hashfun  14403  pr2pwpr  14446  hashtpg  14452  sumpr  15700  lcmfpr  16570  prmreclem2  16856  acsfn2  17613  isdrs2  18265  efmnd2hash  18813  symg2hash  19302  psgnprfval  19432  gsumpr  19866  znidomb  21338  m2detleib  22355  ovolioo  25319  i1f1  25441  itgioo  25567  limcun  25646  aannenlem2  26076  wilthlem2  26807  perfectlem2  26967  upgrex  28617  ex-hash  29971  prodpr  32297  linds2eq  32769  elrspunsn  32819  inelpisys  33448  coinfliplem  33773  coinflippv  33778  subfacp1lem1  34466  poimirlem9  36802  kelac2lem  42110  sumpair  44023  refsum2cnlem1  44025  climxlim2lem  44861  ibliooicc  44987  fourierdlem50  45172  fourierdlem51  45173  fourierdlem54  45176  fourierdlem70  45192  fourierdlem71  45193  fourierdlem76  45198  fourierdlem102  45224  fourierdlem103  45225  fourierdlem104  45226  fourierdlem114  45236  saluncl  45333  sge0pr  45410  meadjun  45478  omeunle  45532  perfectALTVlem2  46690  zlmodzxzel  47121  ldepspr  47243  zlmodzxzldeplem2  47271  rrx2line  47515  2sphere  47524