Metamath Proof Explorer


Theorem snmapen1

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 A V B W A B 1 𝑜

Proof

Step Hyp Ref Expression
1 snmapen A V B W A B A
2 ensn1g A V A 1 𝑜
3 2 adantr A V B W A 1 𝑜
4 entr A B A A 1 𝑜 A B 1 𝑜
5 1 3 4 syl2anc A V B W A B 1 𝑜