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 e. V /\ B e. W ) -> ( { A } ^m B ) ~~ 1o )

Proof

Step	Hyp	Ref	Expression
1		snmapen	|- ( ( A e. V /\ B e. W ) -> ( { A } ^m B ) ~~ { A } )
2		ensn1g	|- ( A e. V -> { A } ~~ 1o )
3	2	adantr	|- ( ( A e. V /\ B e. W ) -> { A } ~~ 1o )
4		entr	|- ( ( ( { A } ^m B ) ~~ { A } /\ { A } ~~ 1o ) -> ( { A } ^m B ) ~~ 1o )
5	1 3 4	syl2anc	|- ( ( A e. V /\ B e. W ) -> ( { A } ^m B ) ~~ 1o )