Description: Set exponentiation: a singleton to any set is equinumerous to ordinal 1. (Proposed by BJ, 17-Jul-2022.) (Contributed by AV, 17-Jul-2022)
Ref | Expression | ||
---|---|---|---|
Assertion | snmapen1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snmapen | ||
2 | ensn1g | ||
3 | 2 | adantr | |
4 | entr | ||
5 | 1 3 4 | syl2anc |