Description: Finitely supported indicator functions are equinumerous to finite subsets.MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015) (Revised by AV, 14-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | pwfi2en.s | ||
Assertion | pwfi2en |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwfi2en.s | ||
2 | eqid | ||
3 | 1 2 | pwfi2f1o | |
4 | ovex | ||
5 | 1 4 | rabex2 | |
6 | 5 | f1oen | |
7 | 3 6 | syl |