![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > prfi | Structured version Visualization version GIF version |
Description: An unordered pair is finite. (Contributed by NM, 22-Aug-2008.) |
Ref | Expression |
---|---|
prfi | ⊢ {𝐴, 𝐵} ∈ Fin |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-pr 4475 | . 2 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵}) | |
2 | snfi 8442 | . . 3 ⊢ {𝐴} ∈ Fin | |
3 | snfi 8442 | . . 3 ⊢ {𝐵} ∈ Fin | |
4 | unfi 8631 | . . 3 ⊢ (({𝐴} ∈ Fin ∧ {𝐵} ∈ Fin) → ({𝐴} ∪ {𝐵}) ∈ Fin) | |
5 | 2, 3, 4 | mp2an 688 | . 2 ⊢ ({𝐴} ∪ {𝐵}) ∈ Fin |
6 | 1, 5 | eqeltri 2879 | 1 ⊢ {𝐴, 𝐵} ∈ Fin |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2081 ∪ cun 3857 {csn 4472 {cpr 4474 Fincfn 8357 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-pss 3876 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-tp 4477 df-op 4479 df-uni 4746 df-int 4783 df-iun 4827 df-br 4963 df-opab 5025 df-mpt 5042 df-tr 5064 df-id 5348 df-eprel 5353 df-po 5362 df-so 5363 df-fr 5402 df-we 5404 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-pred 6023 df-ord 6069 df-on 6070 df-lim 6071 df-suc 6072 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-ov 7019 df-oprab 7020 df-mpo 7021 df-om 7437 df-wrecs 7798 df-recs 7860 df-rdg 7898 df-1o 7953 df-oadd 7957 df-er 8139 df-en 8358 df-fin 8361 |
This theorem is referenced by: tpfi 8640 fiint 8641 inelfi 8728 tskpr 10038 hashpw 13645 hashfun 13646 pr2pwpr 13683 hashtpg 13689 sumpr 14936 lcmfpr 15800 prmreclem2 16082 acsfn2 16763 isdrs2 17378 symg2hash 18256 psgnprfval 18380 gsumpr 18795 znidomb 20390 m2detleib 20924 ovolioo 23852 i1f1 23974 itgioo 24099 limcun 24176 aannenlem2 24601 wilthlem2 25328 perfectlem2 25488 upgrex 26560 ex-hash 27924 prodpr 30226 linds2eq 30587 inelpisys 31030 coinfliplem 31353 coinflippv 31358 subfacp1lem1 32034 poimirlem9 34432 kelac2lem 39149 sumpair 40831 refsum2cnlem1 40833 climxlim2lem 41668 ibliooicc 41797 fourierdlem50 41983 fourierdlem51 41984 fourierdlem54 41987 fourierdlem70 42003 fourierdlem71 42004 fourierdlem76 42009 fourierdlem102 42035 fourierdlem103 42036 fourierdlem104 42037 fourierdlem114 42047 saluncl 42144 sge0pr 42218 meadjun 42286 omeunle 42340 perfectALTVlem2 43369 zlmodzxzel 43881 ldepspr 44008 zlmodzxzldeplem2 44036 rrx2line 44208 2sphere 44217 |
Copyright terms: Public domain | W3C validator |