Theorem cusgrexilem1

Description: Lemma 1 for cusgrexi . (Contributed by Alexander van der Vekens, 12-Jan-2018)

	Ref	Expression
Hypothesis	usgrexi.p	|- P = { x e. ~P V | ( # ` x ) = 2 }
Assertion	cusgrexilem1	|- ( V e. W -> ( _I |` P ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		usgrexi.p	|- P = { x e. ~P V | ( # ` x ) = 2 }
2		pwexg	|- ( V e. W -> ~P V e. _V )
3	1 2	rabexd	|- ( V e. W -> P e. _V )
4		resiexg	|- ( P e. _V -> ( _I |` P ) e. _V )
5	3 4	syl	|- ( V e. W -> ( _I |` P ) e. _V )