Theorem ballotlemoex

Description: O is a set. (Contributed by Thierry Arnoux, 7-Dec-2016)

	Ref	Expression
Hypotheses	ballotth.m	|- M e. NN
	ballotth.n	|- N e. NN
	ballotth.o	|- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
Assertion	ballotlemoex	|- O e. _V

Proof

Step	Hyp	Ref	Expression
1		ballotth.m	|- M e. NN
2		ballotth.n	|- N e. NN
3		ballotth.o	|- O = { c e. ~P ( 1 ... ( M + N ) ) | ( # ` c ) = M }
4		ovex	|- ( 1 ... ( M + N ) ) e. _V
5	4	pwex	|- ~P ( 1 ... ( M + N ) ) e. _V
6	3 5	rabex2	|- O e. _V