MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prfi Structured version   Visualization version   GIF version

Theorem prfi 8441
Description: An unordered pair is finite. (Contributed by NM, 22-Aug-2008.)
Assertion
Ref Expression
prfi {𝐴, 𝐵} ∈ Fin

Proof of Theorem prfi
StepHypRef Expression
1 df-pr 4336 . 2 {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
2 snfi 8244 . . 3 {𝐴} ∈ Fin
3 snfi 8244 . . 3 {𝐵} ∈ Fin
4 unfi 8433 . . 3 (({𝐴} ∈ Fin ∧ {𝐵} ∈ Fin) → ({𝐴} ∪ {𝐵}) ∈ Fin)
52, 3, 4mp2an 683 . 2 ({𝐴} ∪ {𝐵}) ∈ Fin
61, 5eqeltri 2839 1 {𝐴, 𝐵} ∈ Fin
Colors of variables: wff setvar class
Syntax hints:  wcel 2155  cun 3729  {csn 4333  {cpr 4335  Fincfn 8159
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-oadd 7767  df-er 7946  df-en 8160  df-fin 8163
This theorem is referenced by:  tpfi  8442  fiint  8443  inelfi  8530  tskpr  9844  hashpw  13423  hashfun  13424  pr2pwpr  13461  hashtpg  13467  sumpr  14763  lcmfpr  15622  prmreclem2  15901  acsfn2  16590  isdrs2  17206  symg2hash  18081  psgnprfval  18206  znidomb  20181  m2detleib  20713  ovolioo  23625  i1f1  23747  itgioo  23872  limcun  23949  aannenlem2  24374  wilthlem2  25085  perfectlem2  25245  upgrex  26263  ex-hash  27703  prodpr  29955  inelpisys  30598  coinfliplem  30922  coinflippv  30927  subfacp1lem1  31540  poimirlem9  33774  kelac2lem  38243  sumpair  39778  refsum2cnlem1  39780  climxlim2lem  40641  ibliooicc  40756  fourierdlem50  40942  fourierdlem51  40943  fourierdlem54  40946  fourierdlem70  40962  fourierdlem71  40963  fourierdlem76  40968  fourierdlem102  40994  fourierdlem103  40995  fourierdlem104  40996  fourierdlem114  41006  saluncl  41106  sge0pr  41180  meadjun  41248  omeunle  41302  perfectALTVlem2  42239  zlmodzxzel  42734  gsumpr  42740  ldepspr  42863  zlmodzxzldeplem2  42891
  Copyright terms: Public domain W3C validator